1 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
new file mode 100644
index 000000000..bda237676
--- /dev/null
+++ b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=3
+; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
+; SCRUBBER: sed -e 's/.*(>= j (+ 1 1))/SPURIOUS/; s/(define-fun.*//; /^$/d'
+; EXIT: 1
+
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+
+(assert (and (>= n 0) (>= m 0)))
+(assert (< n i))
+(assert (< (+ i j) m))
+
+; This test ensures that (>= j (+ 1 1)) is not printed as a solution,
+; since it is spurious: (>= j 0) is a stronger solution and will be enumerated
+; first.
+(get-abduct A 
+  (<= n m)
+  ((GA Bool) (GI Int))
+  (
+  (GA Bool ((>= GI GI)))
+  (GI Int ((+ GI GI) (- GI) i j 0 1))
+  )
+)