fix (my own) bug in reading off an assignment

vprover · Jul 29, 2024 · 97edbcf · 97edbcf
1 parent 2e1fce3
commit 97edbcf
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/FMB/Monotonicity.cpp b/FMB/Monotonicity.cpp
@@ -74,8 +74,8 @@ DArray<signed char>* Monotonicity::check() {
   DArray<signed char>* res = new DArray<signed char>(env.signature->predicates());
   (*res)[0] = 0; // pick a value for the 0-th = predicate (we don't really care here)
   for(unsigned p=1;p<env.signature->predicates();p++){
-    bool trueExt = _solver->getAssignment(_pT.get(p).var());
-    bool falseExt = _solver->getAssignment(_pF.get(p).var());
+    bool trueExt = _solver->trueInAssignment(_pT.get(p));
+    bool falseExt = _solver->trueInAssignment(_pF.get(p));
     ASS(!trueExt || !falseExt)
     (*res)[p] = trueExt ? 1 : (falseExt ? -1 : 0);
   }