Merge branch 'master' into splitEqRew

1 files changed, 28 insertions, 0 deletions

diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
new file mode 100644
index 000000000..4b7870c78
--- /dev/null
+++ b/test/regress/regress1/sygus-abduct-test-user.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_UFLIRA)
+(set-option :produce-abducts true)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+; Generate a predicate A that is consistent with the above axioms (i.e.
+; their conjunction is SAT), and is such that the conjunction of the above
+; axioms, A and the negation of the conjecture below are UNSAT.
+; The signature of A is below grammar.
+(get-abduct A (not (< x y))
+
+; the grammar for the abduct-to-synthesize
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int (n m (+ StartInt StartInt) 0 1))
+)
+
+)