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.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index ecfa76142338eee724b5b78df64b5709c78eb7f7..140510b3f31a4ae8e4f048b98b039570a6f5c613 100644 (file)
--- 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 14c8ad1ca86a629bbd34b3323966a07d7b80546c..2ce23a3bad562ba175fc690e36e691a46c757804 100644 (file)
--- 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 (file)
index 0000000..73e4311
--- /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)