Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.

1 files changed, 10 insertions, 7 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 4de0d6a54..c064040d9 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -991,13 +991,16 @@ void TheoryEngineModelBuilder::debugCheckModel(Model* m){
       Node n = *eqc_i;
       static int repCheckInstance = 0;
       ++repCheckInstance;
-
-      Debug("check-model::rep-checking")
-        << "( " << repCheckInstance <<") "
-        << "n: " << n << endl
-        << "getValue(n): " << tm->getValue(n) << endl
-        << "rep: " << rep << endl;
-      Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
+      
+      // non-linear mult is not necessarily accurate wrt getValue
+      if( n.getKind()!=kind::NONLINEAR_MULT ){
+        Debug("check-model::rep-checking")
+          << "( " << repCheckInstance <<") "
+          << "n: " << n << endl
+          << "getValue(n): " << tm->getValue(n) << endl
+          << "rep: " << rep << endl;
+        Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
+      }
     }
   }
 #endif /* CVC4_ASSERTIONS */