Fix open proof for factoring lemma (#5885)

We need to add to the current proof, regardless of whether we have used the factor skolem previously.

Fixes bugs found by @HanielB on SMT-LIB runs.

diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 098f4500d619f1fa5c952c68e5fe0c838d736f9f..4a567a0f5446007d3a3bbeb19734ba63def2ccb7 100644 (file)
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -178,22 +178,27 @@ void FactoringCheck::check(const std::vector<Node>& asserts,
 Node FactoringCheck::getFactorSkolem(Node n, CDProof* proof)
 {
   std::map<Node, Node>::iterator itf = d_factor_skolem.find(n);
+  Node k;
   if (itf == d_factor_skolem.end())
   {
     NodeManager* nm = NodeManager::currentNM();
-    Node k = nm->getSkolemManager()->mkPurifySkolem(n, "kf");
+    k = nm->getSkolemManager()->mkPurifySkolem(n, "kf");
     Node k_eq = k.eqNode(n);
     Trace("nl-ext-factor") << "...adding factor skolem " << k << " == " << n
                            << std::endl;
-    if (d_data->isProofEnabled())
-    {
-      proof->addStep(k_eq, PfRule::MACRO_SR_PRED_INTRO, {}, {k_eq});
-    }
     d_data->d_im.addPendingArithLemma(k_eq, InferenceId::NL_FACTOR, proof);
     d_factor_skolem[n] = k;
-    return k;
   }
-  return itf->second;
+  else
+  {
+    k = itf->second;
+  }
+  if (d_data->isProofEnabled())
+  {
+    Node k_eq = k.eqNode(n);
+    proof->addStep(k_eq, PfRule::MACRO_SR_PRED_INTRO, {}, {k_eq});
+  }
+  return k;
 }
 
 }  // namespace nl

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d942ef94068903c25cb251bedbc28c03d7291c61..edf49b502eab106647d3610799f3cd72d21d4514 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1630,6 +1630,7 @@ set(regress_1_tests
   regress1/nl/sugar-ident-3.smt2
   regress1/nl/sugar-ident.smt2
   regress1/nl/tan-rewrite2.smt2
+  regress1/nl/ufnia-factor-open-proof.smt2
   regress1/nl/zero-subset.smt2
   regress1/non-fatal-errors.smt2
   regress1/parsing_ringer.cvc

diff --git a/test/regress/regress1/nl/ufnia-factor-open-proof.smt2 b/test/regress/regress1/nl/ufnia-factor-open-proof.smt2
new file mode 100644 (file)
index 0000000..bcb077f
--- /dev/null
+++ b/test/regress/regress1/nl/ufnia-factor-open-proof.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_UFNIA)
+(set-info :status unsat)
+(declare-fun pow2 (Int) Int)
+(define-fun intmax ((k Int)) Int (- (pow2 k) 1))
+(define-fun intmodtotal ((pow2 Int) (a Int) (b Int)) Int (mod a b))
+(define-fun intneg ((k Int) (a Int)) Int 1)
+(define-fun intmul ((k Int) (a Int) (b Int)) Int (mod (* a b) (pow2 k)))
+(declare-fun k () Int)
+(assert (> k 0))
+(assert (= 1 (pow2 1)))
+(declare-fun %x () Int)
+(assert (> %x 0))
+(assert (not (= (intmul k %x (intmax k)) (mod (- (pow2 k) %x) (pow2 k)))))
+(check-sat)