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 053174d071d32d47f29ab79ef0c2d6ce29a9081d..3a444df93ffd64e6497bbb0f6c29e6d118932535 100644 (file)
--- 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 140978d3db59a2d60e0ae88710025993e8225667..a29c7a9a474a26f92b34a94dc37653e6f71e23f6 100644 (file)
--- 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 (file)
index 0000000..085f58a
--- /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)