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 b14936ee9db30c722b4a4a1b0f4fc780069b6d09..504cafc1690f2ca49ab756ad778285e0b9b55138 100644 (file)
--- 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 c744227e40c2dfde3f6144268d70fa126ad14654..74121ecbd2449e8945e11e0e27d7df45415c0e58 100644 (file)
--- 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 (file)
index 0000000..4b120fc
--- /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)