From 4e2afa2282965f3f54033d43cd990cc0b0a8b200 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Mar 2021 14:11:24 -0600
Subject: [PATCH] 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.
---
 src/theory/quantifiers/fmf/full_model_check.cpp    | 11 +++++++++--
 test/regress/CMakeLists.txt                        |  1 +
 test/regress/regress0/fmf/issue5922-fmf-not-x.smt2 |  8 ++++++++
 3 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/fmf/issue5922-fmf-not-x.smt2

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