From b6df05346a3bd8c1c68ef74635711ff3e6bd5791 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 10 Feb 2021 10:27:44 -0600
Subject: [PATCH] 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.
---
 src/theory/arith/nl/ext/factoring_check.cpp   | 19 ++++++++++++-------
 test/regress/CMakeLists.txt                   |  1 +
 .../regress1/nl/ufnia-factor-open-proof.smt2  | 14 ++++++++++++++
 3 files changed, 27 insertions(+), 7 deletions(-)
 create mode 100644 test/regress/regress1/nl/ufnia-factor-open-proof.smt2

diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 098f4500d..4a567a0f5 100644
--- 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 d942ef940..edf49b502 100644
--- 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
index 000000000..bcb077f4f
--- /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)
-- 
2.30.2