Add regression. (#5994)

This PR adds the test case from #5187 as a regression.
Fixes #5187.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e282deba4997b372c478958912686a971e281ad8..37a9773719f51319a74a2ff049399ce8849e0500 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -637,6 +637,7 @@ set(regress_0_tests
   regress0/issue5099-model-1.smt2
   regress0/issue5099-model-2.smt2
   regress0/issue5144-resetAssertions.smt2
+  regress0/issue5187-div-justification.smt2
   regress0/issue5370.smt2
   regress0/issue5462.smt2
   regress0/issue5540-2-dump-model.smt2

diff --git a/test/regress/regress0/issue5187-div-justification.smt2 b/test/regress/regress0/issue5187-div-justification.smt2
new file mode 100644 (file)
index 0000000..5b6dd6a
--- /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)