From 3809343bf829523e425225cbf641a4fc62c713f7 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 6 Mar 2022 08:02:26 -0800 Subject: [PATCH] Disallow models with `--arrays-weak-equiv` (#8217) Fixes #2007. We currently do not support generating models when `--arrays-weak-equiv` is enabled. This commit adds a corresponding user-facing error message. --- src/smt/set_defaults.cpp | 5 +++++ test/regress/CMakeLists.txt | 1 + .../regress0/arrays/issue8103-1-weak-equiv-models.smt2 | 10 ++++++++++ 3 files changed, 16 insertions(+) create mode 100644 test/regress/regress0/arrays/issue8103-1-weak-equiv-models.smt2 diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index ecfa76142..140510b3f 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -965,6 +965,11 @@ bool SetDefaults::incompatibleWithModels(const Options& opts, reason << "global-negate"; return true; } + else if (opts.arrays.arraysWeakEquivalence) + { + reason << "arrays-weak-equiv"; + return true; + } return false; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 14c8ad1ca..2ce23a3ba 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -127,6 +127,7 @@ set(regress_0_tests regress0/arrays/issue6276.smt2 regress0/arrays/issue6807-idem-rew.smt2 regress0/arrays/issue7596-define-array-uminus.smt2 + regress0/arrays/issue8103-1-weak-equiv-models.smt2 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2 regress0/arrays/x2.smtv1.smt2 regress0/arrays/x3.smtv1.smt2 diff --git a/test/regress/regress0/arrays/issue8103-1-weak-equiv-models.smt2 b/test/regress/regress0/arrays/issue8103-1-weak-equiv-models.smt2 new file mode 100644 index 000000000..73e4311e6 --- /dev/null +++ b/test/regress/regress0/arrays/issue8103-1-weak-equiv-models.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --produce-models --arrays-weak-equiv +; SCRUBBER: grep -o "Cannot use arrays-weak-equiv with model generation" +; EXPECT: Cannot use arrays-weak-equiv with model generation +; EXIT: 1 +(set-logic ALL) +(declare-const a (Array (_ BitVec 64) (_ BitVec 64))) +(declare-const b (_ BitVec 64)) +(assert (= (store a #x1111111111111111 b) + (store a b #x1111111111111111))) +(check-sat) -- 2.30.2