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/regress1/sygus-abduct-test-user.smt2 | |
| parent | 13f6d4b71a194f74001f7a6fbe92bbb2c5c62813 (diff) | |
Flip the polarity of the argument of get-abduct (#3153)
Diffstat (limited to 'test/regress/regress1/sygus-abduct-test-user.smt2')
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test-user.smt2 | 4 |
1 files changed, 2 insertions, 2 deletions
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)) |