diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-02 16:04:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-02 16:04:43 -0500 |
| commit | 902262c421e52405204b3a95310c8414cc51a5c5 (patch) | |
| tree | 51aa57b918c18854223ee21da8d9b4ff352cba93 /test/regress | |
| parent | 13f6d4b71a194f74001f7a6fbe92bbb2c5c62813 (diff) | |
Flip the polarity of the argument of get-abduct (#3153)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress1/sygus-abduct-ex1-grammar.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test-user.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test.smt2 | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 index 17971f184..bda237676 100644 --- a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 +++ b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 @@ -19,7 +19,7 @@ ; since it is spurious: (>= j 0) is a stronger solution and will be enumerated ; first. (get-abduct A - (not (<= n m)) + (<= n m) ((GA Bool) (GI Int)) ( (GA Bool ((>= GI GI))) diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2 index bdb680613..4b7870c78 100644 --- a/test/regress/regress1/sygus-abduct-test-user.smt2 +++ b/test/regress/regress1/sygus-abduct-test-user.smt2 @@ -14,9 +14,9 @@ ; 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 conjecture below are UNSAT. +; axioms, A and the negation of the conjecture below are UNSAT. ; The signature of A is below grammar. -(get-abduct A (< x y) +(get-abduct A (not (< x y)) ; the grammar for the abduct-to-synthesize ((Start Bool) (StartInt Int)) diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2 index d01f5f5ff..ed1ea6ddf 100644 --- a/test/regress/regress1/sygus-abduct-test.smt2 +++ b/test/regress/regress1/sygus-abduct-test.smt2 @@ -13,4 +13,4 @@ (assert (and (<= n x)(<= x (+ n 5)))) (assert (and (<= 1 y)(<= y m))) -(get-abduct A (< x y)) +(get-abduct A (not (< x y))) |