Add regression for fixed issue

ajreynol · Feb 24, 2025 · 5e0f1e0 · 5e0f1e0
1 parent e2d2cfd
commit 5e0f1e0
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -150,6 +150,7 @@ set(regress_0_tests
   regress0/arrays/issue6807-idem-rew.smt2
   regress0/arrays/issue7596-define-array-uminus.smt2
   regress0/arrays/issue8103-1-weak-equiv-models.smt2
+  regress0/arrays/issue8241-bad-model.smt2
   regress0/arrays/issue8276-arith-getModelValue.smt2
   regress0/arrays/issue8810-model-success.smt2
   regress0/arrays/issue9041.smt2

diff --git a/test/regress/cli/regress0/arrays/issue8241-bad-model.smt2 b/test/regress/cli/regress0/arrays/issue8241-bad-model.smt2
@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic ANRA)
+(declare-fun r3 () Real)
+(declare-fun r4 () Real)
+(declare-fun arr () (Array Real Real))
+(assert (and (= r3 (* r4 r3)) (= (* r4 r4) (- (select arr r4)))))
+(assert (and (> r3 1.0) (= 1.0 (select arr 1.0))))
+(check-sat)