From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Mar 2021 20:11:24 +0000 (-0600)
Subject: Fix handling of negation of Boolean bound variables in FMF (#6066)
X-Git-Tag: cvc5-1.0.0~2136
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4e2afa2282965f3f54033d43cd990cc0b0a8b200;p=cvc5.git

Fix handling of negation of Boolean bound variables in FMF (#6066)

Fixes #5922. We were not correctly handling when a Boolean bound variable was negated.
---

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 053174d07..3a444df93 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -982,8 +982,15 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
 
 void FullModelChecker::doNegate( Def & dc ) {
   for (unsigned i=0; i<dc.d_cond.size(); i++) {
-    if (!dc.d_value[i].isNull()) {
-      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i] );
+    Node v = dc.d_value[i];
+    if (!v.isNull())
+    {
+      // In the case that the value is not-constant, we cannot reason about
+      // its value (since the range of this must be a constant or variable).
+      // In particular, returning null here is important if we have (not x)
+      // where x is a bound variable.
+      dc.d_value[i] =
+          v == d_true ? d_false : (v == d_false ? d_true : Node::null());
     }
   }
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 140978d3d..a29c7a9a4 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -555,6 +555,7 @@ set(regress_0_tests
   regress0/fmf/issue4850-force-card.smt2
   regress0/fmf/issue4872-qf_ufc.smt2
   regress0/fmf/issue5239-uf-ss-tot.smt2
+  regress0/fmf/issue5922-fmf-not-x.smt2
   regress0/fmf/krs-sat.smt2
   regress0/fmf/no-minimal-sat.smt2
   regress0/fmf/QEpres-uf.855035.smtv1.smt2
diff --git a/test/regress/regress0/fmf/issue5922-fmf-not-x.smt2 b/test/regress/regress0/fmf/issue5922-fmf-not-x.smt2
new file mode 100644
index 000000000..085f58a26
--- /dev/null
+++ b/test/regress/regress0/fmf/issue5922-fmf-not-x.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun f (Bool) Bool)
+(assert (forall ((x Bool)) (f (not x))))
+(assert (=> (f true) false))
+(check-sat)