From 5e0f1e06c57776f3a974054b6e647ddf22490341 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 24 Feb 2025 09:37:04 -0600 Subject: [PATCH] Add regression for fixed issue --- test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress0/arrays/issue8241-bad-model.smt2 | 8 ++++++++ 2 files changed, 9 insertions(+) create mode 100644 test/regress/cli/regress0/arrays/issue8241-bad-model.smt2 diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 66b34a998c0..ea26de638d3 100644 --- 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 new file mode 100644 index 00000000000..222da90c129 --- /dev/null +++ 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)