diff --git a/forge/sigs.rkt b/forge/sigs.rkt index 2cd41f15..045c4c0d 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -630,6 +630,7 @@ (syntax-parse stx [(_ name:id pred bounds ...) (add-to-execs + (with-syntax ([double-check-name (format-id #'name "double-check_~a_~a" #'name (gensym))]) (quasisyntax/loc stx (begin (when (eq? 'temporal (get-option curr-state 'problem_type)) (raise-forge-error @@ -638,8 +639,8 @@ #,(syntax/loc stx (run name #:preds [pred] #:bounds [bounds ...])) (define first-instance (tree:get-value (Run-result name))) (when (Unsat? first-instance) - #,(syntax/loc stx (run double-check #:preds [] #:bounds [bounds ...])) - (define double-check-instance (tree:get-value (Run-result double-check))) + #,(syntax/loc stx (run double-check-name #:preds [] #:bounds [bounds ...])) + (define double-check-instance (tree:get-value (Run-result double-check-name))) (if (Sat? double-check-instance) (report-test-failure #:name 'name #:msg (format "Invalid example '~a'; the instance specified does not satisfy the given predicate." 'name) #:context #,(build-source-location stx) @@ -651,7 +652,7 @@ 'name) #:context #,(build-source-location stx) #:instance first-instance - #:run name))))))])) + #:run name)))))))])) ; Checks that some predicates are always true. ; (check name diff --git a/forge/tests/error/main.rkt b/forge/tests/error/main.rkt index 502ce598..bd12e7fe 100644 --- a/forge/tests/error/main.rkt +++ b/forge/tests/error/main.rkt @@ -34,6 +34,7 @@ (list "hidden-wheat.frg" #rx"Invalid binding expression") (list "unstated_bounds.frg" #rx"Scope for Match was not declared") + (list "multiple-positive-examples-failing.frg" #rx"Invalid example 'e1'.*?Invalid example 'e2'") (list "abstract.frg" #rx"abstract") (list "bsl-ast-arrow.frg" #rx"Direct use of ->") diff --git a/forge/tests/error/multiple-positive-examples-failing.frg b/forge/tests/error/multiple-positive-examples-failing.frg new file mode 100644 index 00000000..a5abb2a8 --- /dev/null +++ b/forge/tests/error/multiple-positive-examples-failing.frg @@ -0,0 +1,14 @@ +#lang forge +option run_sterling off +option verbose 0 + +-- Regression test to confirm that the "double-check" done in example tests +-- isn't duplicating run names (and causing an error that prevents multiple +-- examples from running). + +sig Node {} +pred someNode { some Node } +example e1 is {someNode} for { no Node } -- failure; do a double-check +example e2 is someNode for { no Node } -- failure; do another double-check + +