Do not use factoring inference for transcendental functions (#1707)

2 files changed, 21 insertions, 4 deletions

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 07cf43a35..38b53e107 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -2886,9 +2886,23 @@ std::vector<Node> NonlinearExtension::checkFactoring(
   {
     bool polarity = lit.getKind() != NOT;
     Node atom = lit.getKind() == NOT ? lit[0] : lit;
-    if (std::find(false_asserts.begin(), false_asserts.end(), lit)
-            != false_asserts.end()
-        || d_skolem_atoms.find(atom) != d_skolem_atoms.end())
+    Node litv = computeModelValue(lit);
+    bool considerLit = false;
+    if( d_skolem_atoms.find(atom) != d_skolem_atoms.end() )
+    {
+      //always consider skolem literals
+      considerLit = true;
+    }
+    else
+    {
+      // Only consider literals that evaluate to false in the model.
+      // this is a stronger restriction than the restriction that lit is in
+      // false_asserts.
+      // This excludes (most) literals that contain transcendental functions.
+      considerLit = computeModelValue(lit)==d_false;
+    }
+
+    if (considerLit)
     {
       std::map<Node, Node> msum;
       if (ArithMSum::getMonomialSumLit(atom, msum))
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 96d37cbc2..8b1a320a2 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -426,7 +426,10 @@ class NonlinearExtension {
   /** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */
   NodeSet d_zero_split;
   
-  // literals with Skolems (need not be satisfied by model)
+  /** 
+   * The set of atoms with Skolems that this solver introduced. We do not
+   * require that models satisfy literals over Skolem atoms.
+   */
   NodeSet d_skolem_atoms;
 
   /** commonly used terms */