diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-25 14:34:40 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-25 14:34:40 +0100 |
| commit | 73e83f6350915e52fbc29f69da24b1507fce1c9f (patch) | |
| tree | b8a883a0106794ea8c11f1a4af01393bd963ac2e /test/regress/regress0 | |
| parent | ca532e04c4b484bbd5c99e0da62e07814dd77d6d (diff) | |
Add regression. (#5994)
This PR adds the test case from #5187 as a regression.
Fixes #5187.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/issue5187-div-justification.smt2 | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress0/issue5187-div-justification.smt2 b/test/regress/regress0/issue5187-div-justification.smt2 new file mode 100644 index 000000000..5b6dd6a27 --- /dev/null +++ b/test/regress/regress0/issue5187-div-justification.smt2 @@ -0,0 +1,32 @@ +; COMMAND-LINE: --strings-exp -i +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: sat +(set-logic QF_AUFNIA) +(declare-fun _substvar_77_ () Int) +(declare-fun _substvar_82_ () Int) +(declare-const v11 Bool) +(declare-const arr (Array Bool Int)) +(push 1) +(declare-const i3 Int) +(declare-const i5 Int) +(assert (= (* 469 _substvar_77_) (div 174 (div 81 81)))) +(push 1) +(assert (< 0 (* i5 i3 469 (select (store arr true 81) v11) (+ _substvar_82_ 174 81)))) +(push 1) +(push 1) +(check-sat) +(pop 1) +(pop 1) +(push 1) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(pop 1) +(check-sat) +(pop 1) +(pop 1) +(check-sat) |