fix: double-check runs for failing examples need de-duplicated names

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

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 ->")

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
+
+