From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jan 2020 20:05:06 +0000 (-0600)
Subject: Ensure literals in FMF decision strategies are in the CNF stream (#3669)
X-Git-Tag: cvc5-1.0.0~3707
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=164e5274e3135b245b8ce5576841bb6c329eecfe;p=cvc5.git

Ensure literals in FMF decision strategies are in the CNF stream (#3669)
---

diff --git a/src/theory/decision_strategy.cpp b/src/theory/decision_strategy.cpp
index b14936ee9..504cafc16 100644
--- a/src/theory/decision_strategy.cpp
+++ b/src/theory/decision_strategy.cpp
@@ -114,11 +114,16 @@ Node DecisionStrategyFmf::getLiteral(unsigned n)
     if (!lit.isNull())
     {
       lit = Rewriter::rewrite(lit);
-      lit = d_valuation.ensureLiteral(lit);
     }
     d_literals.push_back(lit);
   }
-  return d_literals[n];
+  Node ret = d_literals[n];
+  if (!ret.isNull())
+  {
+    // always ensure it is in the CNF stream
+    ret = d_valuation.ensureLiteral(ret);
+  }
+  return ret;
 }
 
 DecisionStrategySingleton::DecisionStrategySingleton(
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c744227e4..74121ecbd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -460,6 +460,7 @@ set(regress_0_tests
   regress0/fmf/fmc_unsound_model.smt2
   regress0/fmf/fmf-strange-bounds-2.smt2
   regress0/fmf/forall_unit_data2.smt2
+  regress0/fmf/issue3661-ccard-dec.smt2
   regress0/fmf/krs-sat.smt2
   regress0/fmf/no-minimal-sat.smt2
   regress0/fmf/quant_real_univ.cvc
diff --git a/test/regress/regress0/fmf/issue3661-ccard-dec.smt2 b/test/regress/regress0/fmf/issue3661-ccard-dec.smt2
new file mode 100644
index 000000000..4b120fc9d
--- /dev/null
+++ b/test/regress/regress0/fmf/issue3661-ccard-dec.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --fmf-fun -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a (Int) Bool)
+(declare-fun b (Int) Bool)
+(assert (= (a 0) (b 0)))
+(push)
+(check-sat)
+(pop)
+(check-sat)