Fix getModelValue for arithmetic (#8316)

Fixes #8276.

Theory::getModelValue is used as an optimization for computing the care graph of arrays. This method was wrong for (non-linear) arithmetic when the NL extension repaired values in the model.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 252dd5d54d160bcb018da93e3fe4ba5c93e55fcf..624a7d7cda99d3a4ad1cb3a7a93d97e5ed0151f0 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -353,6 +353,11 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
 }
 
 Node TheoryArith::getModelValue(TNode var) {
+  std::map<Node, Node>::iterator it = d_arithModelCache.find(var);
+  if (it != d_arithModelCache.end())
+  {
+    return it->second;
+  }
   return d_internal->getModelValue( var );
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 32604095fc0a78a49bc7e873a36683682f4f9cca..eaeaebdbcc5ab8652659db92112d5671687ea68e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -129,6 +129,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/issue8276-arith-getModelValue.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/issue8276-arith-getModelValue.smt2 b/test/regress/regress0/arrays/issue8276-arith-getModelValue.smt2
new file mode 100644 (file)
index 0000000..c511a92
--- /dev/null
+++ b/test/regress/regress0/arrays/issue8276-arith-getModelValue.smt2
@@ -0,0 +1,10 @@
+(set-logic ANRA)
+(set-info :status sat)
+(declare-fun r4 () Real)
+(declare-fun r9 () Real)
+(declare-fun arr () (Array Bool (Array Real Real)))
+(declare-fun r38 () Real)
+(assert (< r38 r9))
+(assert (= 1.0 (* r4 (select (select arr true) 0.0))))
+(assert (= 0.0 (* r9 (select (select arr true) r9))))
+(check-sat)