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 | |
| parent | 3ee5f2212f287046ab9cda62174eb58ea9561d42 (diff) | |
Fix for learned rewrite pass, add regression (#6850)
Fixes #4791.
| -rw-r--r-- | src/preprocessing/passes/learned_rewrite.cpp | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue4791-llr.smt2 | 21 |
3 files changed, 23 insertions, 1 deletions
diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp index fd3cf832b..81fbf1ea1 100644 --- a/src/preprocessing/passes/learned_rewrite.cpp +++ b/src/preprocessing/passes/learned_rewrite.cpp @@ -293,7 +293,7 @@ Node LearnedRewrite::rewriteLearned(Node n, || (!db.upper_value.isNull() && db.upper_value.getConst<Rational>().sgn() == -1)) { - Rational bden = db.lower_value.isNull() + Rational bden = db.upper_value.isNull() ? db.lower_value.getConst<Rational>() : db.upper_value.getConst<Rational>().abs(); // if 0 <= UB(num) < LB(den) or 0 <= UB(num) < -UB(den) 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) |