diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-12 14:18:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-12 19:18:17 +0000 |
commit | 7d1c5cbef46f316d044a73ad11fac8a64c864f2c (patch) | |
tree | b463b0b315dd2c7b7a9b270aa0ed450c94871fe8 /test | |
parent | 3ee5f2212f287046ab9cda62174eb58ea9561d42 (diff) |
Fix for learned rewrite pass, add regression (#6850)
Fixes #4791.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/nl/issue4791-llr.smt2 | 21 |
2 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cdc77c980..be0815668 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1676,6 +1676,7 @@ set(regress_1_tests regress1/nl/issue3656.smt2 regress1/nl/issue3803-nl-check-model.smt2 regress1/nl/issue3955-ee-double-notify.smt2 + regress1/nl/issue4791-llr.smt2 regress1/nl/issue5372-2-no-m-presolve.smt2 regress1/nl/issue5662-nl-tc.smt2 regress1/nl/issue5662-nl-tc-min.smt2 diff --git a/test/regress/regress1/nl/issue4791-llr.smt2 b/test/regress/regress1/nl/issue4791-llr.smt2 new file mode 100644 index 000000000..d29a16313 --- /dev/null +++ b/test/regress/regress1/nl/issue4791-llr.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --learned-rewrite --no-check-unsat-cores +; EXPECT: unsat +; +;!(a,b,c).( 0<=b & 1<=c & 0<=a & 1<=c +; => +; (a+(b mod c)) mod c = (a+b) mod c) +; +(set-logic QF_NIA) +(set-option :print-success false) + +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) + +(assert (<= 0 a)) +(assert (<= 1 c)) +(assert (<= 0 b)) + +(assert (! (not (= (mod (+ a (mod b c)) c) (mod (+ a b) c))) :named goal)) +(check-sat) +(exit) |