From 73e83f6350915e52fbc29f69da24b1507fce1c9f Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 25 Feb 2021 14:34:40 +0100
Subject: [PATCH] Add regression. (#5994)

This PR adds the test case from #5187 as a regression.
Fixes #5187.
---
 test/regress/CMakeLists.txt                   |  1 +
 .../regress0/issue5187-div-justification.smt2 | 32 +++++++++++++++++++
 2 files changed, 33 insertions(+)
 create mode 100644 test/regress/regress0/issue5187-div-justification.smt2

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e282deba4..37a977371 100644
--- 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
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)
-- 
2.30.2