From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 6 Mar 2022 16:02:26 +0000 (-0800)
Subject: Disallow models with `--arrays-weak-equiv` (#8217)
X-Git-Tag: cvc5-1.0.0~313
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3809343bf829523e425225cbf641a4fc62c713f7;p=cvc5.git

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 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)