diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-24 16:24:25 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-24 15:24:25 +0000 |
| commit | cfe207563479a1e9e13d52bdd93446a8c816636a (patch) | |
| tree | b627d7b238df9ba500cc63ef7ddee62f3bc96d3f /test | |
| parent | 31bba4ba83354f41c756e9800489672ff1c9711c (diff) | |
Only consider relevant terms for integer branches (#6181)
Linear arithmetic simply tried to branch on the first integer variable that had a non-integral assignment.
If it holds stale variables that are not part of the current input, these branches can be emitted and are processed by the solver, but the resulting new assertions will not be considered relevant and thus not added to the theory.
As it still triggers a new theory check, linear arithmetic repeats the same procedure and causes an infinite loop.
This PR explicitly tracks the currently relevant nodes by storing all preregistered nodes and only allows branching on variables from this set.
Fixes #6146.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/integers/issue6146-stale-vars.smt2 | 18 |
2 files changed, 19 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2aa8861fd..c7d97d0fd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -51,6 +51,7 @@ set(regress_0_tests regress0/arith/integers/arith-int-042.min.cvc regress0/arith/integers/arith-int-079.cvc regress0/arith/integers/arith-interval.cvc + regress0/arith/integers/issue6146-stale-vars.smt2 regress0/arith/issue1399.smt2 regress0/arith/issue3412.smt2 regress0/arith/issue3413.smt2 diff --git a/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2 b/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2 new file mode 100644 index 000000000..3f23e0367 --- /dev/null +++ b/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: -i --check-models +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic NIRA) +(declare-fun i8 () Int) +(declare-fun i12 () Int) +(declare-fun r11 () Real) +(declare-fun r18 () Real) +(declare-fun i19 () Int) +(push) +(assert (= 1 (* i8 (to_int r18)))) +(check-sat) +(pop) +(assert (is_int (- r18))) +(check-sat) +(assert (and (< i12 i19) (< 0 (+ i12 2)) (= i19 (* 3 (to_int r11))))) +(check-sat) |