From 85ab7cba7ebf1fa989777f074cb850949f861e93 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Mar 2022 19:42:37 -0600 Subject: [PATCH] Add regression for fixed issue 6700 (#8265) Fixes #6700. --- test/regress/CMakeLists.txt | 1 + .../arrays/issue6700-inc-check-model.smt2 | 17 +++++++++++++++++ 2 files changed, 18 insertions(+) create mode 100644 test/regress/regress0/arrays/issue6700-inc-check-model.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6e8f5a774..474f44640 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -125,6 +125,7 @@ set(regress_0_tests regress0/arrays/issue5836.smt2 regress0/arrays/issue6276-2.smt2 regress0/arrays/issue6276.smt2 + regress0/arrays/issue6700-inc-check-model.smt2 regress0/arrays/issue6807-idem-rew.smt2 regress0/arrays/issue7596-define-array-uminus.smt2 regress0/arrays/issue8103-1-weak-equiv-models.smt2 diff --git a/test/regress/regress0/arrays/issue6700-inc-check-model.smt2 b/test/regress/regress0/arrays/issue6700-inc-check-model.smt2 new file mode 100644 index 000000000..96494f539 --- /dev/null +++ b/test/regress/regress0/arrays/issue6700-inc-check-model.smt2 @@ -0,0 +1,17 @@ +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_ALIA) +(set-option :incremental true) +(declare-fun v4 () Bool) +(declare-fun v6 () Bool) +(declare-fun v9 () Bool) +(declare-fun i () Int) +(declare-fun a () (Array Int Bool)) +(declare-fun v () Bool) +(declare-fun v2 () Bool) +(assert (xor v9 v9 v6 v2 v4 v (select (store a i false) 1) (select a 1))) +(push) +(assert (= i 0)) +(check-sat) +(assert (not (xor v6 v2 v4 v (select a 1) (select a 1)))) +(check-sat) -- 2.30.2