add: draft bdd model, prob needs another pass

tnelson · Feb 24, 2025 · b938c23 · b938c23
1 parent 5bf2358
commit b938c23
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/forge/examples/README.md b/forge/examples/README.md
@@ -24,8 +24,6 @@ While many of these examples are commented heavily, the [Forge documentation](ht
 * `examples/ltlf` contains a model of finite-trace linear temporal logic. 
 * `examples/network` contains a basic model of network forwarding. 
 
-
-
 For more advanced examples, see: 
 
 * `examples/prim`, which contains a model of Prim's MST algorithm, with notes on verification.

diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt
@@ -437,7 +437,7 @@
       (define codomain-type (expression-type-type (checkExpression run-or-state (mexpr-expr codomain) quantvars checker-hash)))
       (if (not (member (car output-type) codomain-type))
           (raise-forge-error
-          #:msg (format "The output of function ~a is of incorrect type. Got ~a, expected in ~a" name (car output-type) codomain-type)
+          #:msg (format "The output of function ~a is of incorrect type. Got ~a, expected in ~a" name output-type codomain-type)
           #:context expanded)
           (void))
        (checkExpression-mult run-or-state expanded quantvars checker-hash)]