Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.

35 files changed, 2085 insertions, 774 deletions

diff --git a/src/options/arith_options b/src/options/arith_options
index 32310a495..bddde7a16 100644
--- a/src/options/arith_options
+++ b/src/options/arith_options
@@ -171,6 +171,9 @@ option nlExt --nl-ext bool :default true
 option nlExtResBound --nl-ext-rbound bool :default false
  use resolution-style inference for inferring new bounds
 
+option nlExtFactor --nl-ext-factor bool :default true
+ use factoring inference in non-linear solver
+ 
 option nlExtTangentPlanes --nl-ext-tplanes bool :default false
  use non-terminating tangent plane strategy for non-linear
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index fe5eb3ac8..674dbe49d 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -53,6 +53,12 @@ void Smt2::addArithmeticOperators() {
   Parser::addOperator(kind::LEQ);
   Parser::addOperator(kind::GT);
   Parser::addOperator(kind::GEQ);
+  
+  addOperator(kind::POW, "^");
+  addOperator(kind::EXPONENTIAL, "exp");
+  addOperator(kind::SINE, "sin");
+  addOperator(kind::COSINE, "cos");
+  addOperator(kind::TANGENT, "tan");
 }
 
 void Smt2::addBitvectorOperators() {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 074041262..2ba593377 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -383,6 +383,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::PLUS:
   case kind::MULT:
   case kind::NONLINEAR_MULT:
+  case kind::EXPONENTIAL:
+  case kind::SINE:
+  case kind::COSINE:
+  case kind::TANGENT:
   case kind::MINUS:
   case kind::UMINUS:
   case kind::LT:
@@ -817,6 +821,10 @@ static string smtKindString(Kind k) throw() {
   case kind::PLUS: return "+";
   case kind::MULT:
   case kind::NONLINEAR_MULT: return "*";
+  case kind::EXPONENTIAL: return "exp";
+  case kind::SINE: return "sin";
+  case kind::COSINE: return "cos";
+  case kind::TANGENT: return "tan";
   case kind::MINUS: return "-";
   case kind::UMINUS: return "-";
   case kind::LT: return "<";
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 4684ec4a3..57428d209 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -101,7 +101,12 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
       return preRewritePlus(t);
     case kind::MULT:
     case kind::NONLINEAR_MULT:
-      return preRewriteMult(t);
+      return preRewriteMult(t);  
+    case kind::EXPONENTIAL:
+    case kind::SINE:
+    case kind::COSINE:
+    case kind::TANGENT:
+      return preRewriteTranscendental(t);
     case kind::INTS_DIVISION:
     case kind::INTS_MODULUS:
       return RewriteResponse(REWRITE_DONE, t);
@@ -126,6 +131,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
       return RewriteResponse(REWRITE_DONE, t[0]);
     case kind::POW:
       return RewriteResponse(REWRITE_DONE, t);
+    case kind::PI:
+      return RewriteResponse(REWRITE_DONE, t);
     default:
       Unhandled(k);
     }
@@ -150,7 +157,12 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       return postRewritePlus(t);
     case kind::MULT:
     case kind::NONLINEAR_MULT:
-      return postRewriteMult(t);
+      return postRewriteMult(t);    
+    case kind::EXPONENTIAL:
+    case kind::SINE:
+    case kind::COSINE:
+    case kind::TANGENT:
+      return postRewriteTranscendental(t);
     case kind::INTS_DIVISION:
     case kind::INTS_MODULUS:
       return RewriteResponse(REWRITE_DONE, t);
@@ -197,15 +209,21 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
           if(exp.sgn() == 0){
             return RewriteResponse(REWRITE_DONE, mkRationalNode(Rational(1)));
           }else if(exp.sgn() > 0 && exp.isIntegral()){
-            Integer num = exp.getNumerator();
-            NodeBuilder<> nb(kind::MULT);
-            Integer one(1);
-            for(Integer i(0); i < num; i = i + one){
-              nb << base;
+            CVC4::Rational r(INT_MAX);
+            if( exp<r ){
+              unsigned num = exp.getNumerator().toUnsignedInt();
+              if( num==1 ){
+                return RewriteResponse(REWRITE_AGAIN, base);
+              }else{
+                NodeBuilder<> nb(kind::MULT);
+                for(unsigned i=0; i < num; ++i){
+                  nb << base;
+                }
+                Assert(nb.getNumChildren() > 0);
+                Node mult = nb;
+                return RewriteResponse(REWRITE_AGAIN, mult);
+              }
             }
-            Assert(nb.getNumChildren() > 0);
-            Node mult = nb;
-            return RewriteResponse(REWRITE_AGAIN, mult);
           }
         }
 
@@ -216,6 +234,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
         ss << "  " << t;
         throw LogicException(ss.str());
       }
+    case kind::PI:
+      return RewriteResponse(REWRITE_DONE, t);
     default:
       Unreachable();
     }
@@ -332,6 +352,100 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
   return RewriteResponse(REWRITE_DONE, res.getNode());
 }
 
+
+RewriteResponse ArithRewriter::preRewriteTranscendental(TNode t) {
+  return RewriteResponse(REWRITE_DONE, t);
+}
+
+RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { 
+  Trace("arith-tf-rewrite") << "Rewrite transcendental function : " << t << std::endl;
+  switch( t.getKind() ){
+  case kind::EXPONENTIAL: {
+    if(t[0].getKind() == kind::CONST_RATIONAL){
+      Node one = NodeManager::currentNM()->mkConst(Rational(1));
+      if(t[0].getConst<Rational>().sgn()>=0 && t[0].getType().isInteger() && t[0]!=one){
+        return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::POW, NodeManager::currentNM()->mkNode( kind::EXPONENTIAL, one ), t[0]));
+      }else{          
+        return RewriteResponse(REWRITE_DONE, t);
+      }
+    }else if(t[0].getKind() == kind::PLUS ){
+      std::vector<Node> product;
+      for( unsigned i=0; i<t[0].getNumChildren(); i++ ){
+        product.push_back( NodeManager::currentNM()->mkNode( kind::EXPONENTIAL, t[0][i] ) );
+      }
+      return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::MULT, product));
+    }
+  }
+    break;
+  case kind::SINE:
+    if(t[0].getKind() == kind::CONST_RATIONAL){
+      const Rational& rat = t[0].getConst<Rational>();
+      if(rat.sgn() == 0){
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(0)));
+      }
+    }else{
+      Node pi_factor;
+      Node pi;
+      if( t[0].getKind()==kind::PI ){
+        pi_factor = NodeManager::currentNM()->mkConst(Rational(1));
+        pi = t[0];
+      }else if( t[0].getKind()==kind::MULT && t[0][0].isConst() && t[0][1].getKind()==kind::PI ){
+        pi_factor = t[0][0];
+        pi = t[0][1];
+      }
+      if( !pi_factor.isNull() ){
+        Trace("arith-tf-rewrite-debug") << "Process pi factor = " << pi_factor << std::endl;
+        Rational r = pi_factor.getConst<Rational>();
+        Rational ra = r.abs();
+        Rational rone = Rational(1);
+        Node ntwo = NodeManager::currentNM()->mkConst( Rational(2) );
+        if( ra > rone ){
+          //add/substract 2*pi beyond scope
+          Node ra_div_two = NodeManager::currentNM()->mkNode( kind::INTS_DIVISION, NodeManager::currentNM()->mkConst( ra + rone ), ntwo );
+          Node new_pi_factor;
+          if( r.sgn()==1 ){
+            new_pi_factor = NodeManager::currentNM()->mkNode( kind::MINUS, pi_factor, NodeManager::currentNM()->mkNode( kind::MULT, ntwo, ra_div_two ) );
+          }else{
+            Assert( r.sgn()==-1 );
+            new_pi_factor = NodeManager::currentNM()->mkNode( kind::PLUS, pi_factor, NodeManager::currentNM()->mkNode( kind::MULT, ntwo, ra_div_two ) );
+          }
+          return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode( kind::SINE,
+                                                       NodeManager::currentNM()->mkNode( kind::MULT, new_pi_factor, pi ) ) );
+        }else if( ra == rone ){
+          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(0)));
+        }else{
+          Integer one = Integer(1);
+          Integer two = Integer(2);
+          Integer six = Integer(6);
+          if( ra.getDenominator()==two ){
+            return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst( Rational( r.sgn() ) ) );
+          }else if( ra.getDenominator()==six ){
+            Integer five = Integer(5);
+            if( ra.getNumerator()==one || ra.getNumerator()==five ){
+              return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst( Rational( r.sgn() )/Rational(2) ) );
+            }
+          }
+        }
+      }
+    }
+    break;
+  case kind::COSINE: {
+    return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode( kind::SINE, 
+                                                 NodeManager::currentNM()->mkNode( kind::MINUS, 
+                                                   NodeManager::currentNM()->mkNode( kind::MULT, 
+                                                     NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ),
+                                                     NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI ) ),
+                                                     t[0] ) ) );
+  } break;
+  case kind::TANGENT:
+    return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode(kind::DIVISION, NodeManager::currentNM()->mkNode( kind::SINE, t[0] ), 
+                                                                                           NodeManager::currentNM()->mkNode( kind::COSINE, t[0] ) ));
+  default:
+    break;
+  }
+  return RewriteResponse(REWRITE_DONE, t);
+}
+
 RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
   if(atom.getKind() == kind::IS_INTEGER) {
     if(atom[0].isConst()) {
@@ -440,7 +554,6 @@ Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
 RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre){
   Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind()== kind::DIVISION);
 
-
   Node left = t[0];
   Node right = t[1];
   if(right.getKind() == kind::CONST_RATIONAL){
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 38b6c9451..a4472d6c3 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -57,7 +57,9 @@ private:
 
   static RewriteResponse preRewriteMult(TNode t);
   static RewriteResponse postRewriteMult(TNode t);
-
+  
+  static RewriteResponse preRewriteTranscendental(TNode t);
+  static RewriteResponse postRewriteTranscendental(TNode t);
 
   static RewriteResponse preRewriteAtom(TNode t);
   static RewriteResponse postRewriteAtom(TNode t);
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 04d8d50ea..f6e702f5b 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -43,6 +43,8 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa
     d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
 {
   d_ee.addFunctionKind(kind::NONLINEAR_MULT);
+  d_ee.addFunctionKind(kind::EXPONENTIAL);
+  d_ee.addFunctionKind(kind::SINE);
   //module to infer additional equalities based on normalization
   if( options::sNormInferEq() ){
     d_eq_infer = new quantifiers::EqualityInference(c, true);
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 61029ac48..0884083c0 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -27,6 +27,11 @@ operator ABS 1 "absolute value"
 parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term"
 operator POW 2 "arithmetic power"
 
+operator EXPONENTIAL 1 "exponential"
+operator SINE 1 "sine"
+operator COSINE 1 "consine"
+operator TANGENT 1 "tangent"
+
 constant DIVISIBLE_OP \
         ::CVC4::Divisible \
         ::CVC4::DivisibleHashFunction \
@@ -112,4 +117,13 @@ typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
 typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
 
+typerule EXPONENTIAL ::CVC4::theory::arith::RealOperatorTypeRule
+typerule SINE ::CVC4::theory::arith::RealOperatorTypeRule
+typerule COSINE ::CVC4::theory::arith::RealOperatorTypeRule
+typerule TANGENT ::CVC4::theory::arith::RealOperatorTypeRule
+
+nullaryoperator PI "pi"
+
+typerule PI ::CVC4::theory::arith::RealNullaryOperatorTypeRule
+
 endtheory
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 02266f331..42f9636dc 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -217,6 +217,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                        eq::EqualityEngine* ee)
     : d_lemmas(containing.getUserContext()),
       d_zero_split(containing.getUserContext()),
+      d_skolem_atoms(containing.getUserContext()),
       d_containing(containing),
       d_ee(ee),
       d_needsLastCall(false) {
@@ -235,7 +236,7 @@ NonlinearExtension::~NonlinearExtension() {}
 // Returns a reference to either map[key] if it exists in the map
 // or to a default value otherwise.
 //
-// Warning: special care must be taken if value is a temporary object.
+// Warning: sped_cial care must be taken if value is a temporary object.
 template <class MapType, class Key, class Value>
 const Value& FindWithDefault(const MapType& map, const Key& key,
                              const Value& value) {
@@ -699,49 +700,58 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) {
   if (it != d_mv[index].end()) {
     return it->second;
   } else {
-    Trace("nl-ext-debug") << "computeModelValue " << n << std::endl;
+    Trace("nl-ext-mv-debug") << "computeModelValue " << n << ", index=" << index << std::endl;
     Node ret;
     if (n.isConst()) {
       ret = n;
-    } else {
-      if (n.getNumChildren() == 0) {
-        ret = d_containing.getValuation().getModel()->getValue(n);
+    } else if (index == 1 && ( n.getKind() == kind::NONLINEAR_MULT || isTranscendentalKind( n.getKind() ) )) {
+      if (d_containing.getValuation().getModel()->hasTerm(n)) {
+        // use model value for abstraction
+        ret = d_containing.getValuation().getModel()->getRepresentative(n);
       } else {
-        if (index == 1 && n.getKind() == kind::NONLINEAR_MULT) {
-          if (d_containing.getValuation().getModel()->hasTerm(n)) {
-            // use model value for abstraction
-            ret = d_containing.getValuation().getModel()->getRepresentative(n);
-          } else {
-            // abstraction does not exist, use concrete
-            ret = computeModelValue(n, 0);
-          }
-        } else {
-          // otherwise, compute true value
-          std::vector<Node> children;
-          if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-            children.push_back(n.getOperator());
-          }
-          for (unsigned i = 0; i < n.getNumChildren(); i++) {
-            Node mc = computeModelValue(n[i], index);
-            children.push_back(mc);
-          }
-          ret = Rewriter::rewrite(
-              NodeManager::currentNM()->mkNode(n.getKind(), children));
-          if (!ret.isConst()) {
-            Trace("nl-ext-debug") << "...got non-constant : " << ret << " for "
-                                  << n << ", ask model directly." << std::endl;
-            ret = d_containing.getValuation().getModel()->getValue(ret);
-          }
-        }
+        // abstraction does not exist, use model value
+        //ret = computeModelValue(n, 0);
+        ret = d_containing.getValuation().getModel()->getValue(n);
       }
-      if (ret.getType().isReal() && !isArithKind(n.getKind())) {
-        // Trace("nl-ext-mv-debug") << ( index==0 ? "M" : "M_A" ) << "[ " << n
-        // << " ] -> " << ret << std::endl;
-        Assert(ret.isConst());
+      //Assert( ret.isConst() );
+    } else if (n.getNumChildren() == 0) {
+      if( n.getKind()==kind::PI ){
+        ret = n;
+      }else{
+        ret = d_containing.getValuation().getModel()->getValue(n);
+      }
+    } else {    
+      // otherwise, compute true value
+      std::vector<Node> children;
+      if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        children.push_back(n.getOperator());
+      }
+      for (unsigned i = 0; i < n.getNumChildren(); i++) {
+        Node mc = computeModelValue(n[i], index);
+        children.push_back(mc);
+      }
+      ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+      if( n.getKind()==kind::APPLY_UF ){
+        ret = d_containing.getValuation().getModel()->getValue(ret);
+      }else{
+        ret = Rewriter::rewrite(ret);
+      }
+          /*
+      if (!ret.isConst()) {
+        Trace("nl-ext-debug") << "...got non-constant : " << ret << " for "
+                              << n << ", ask model directly." << std::endl;
+        ret = d_containing.getValuation().getModel()->getValue(ret);
       }
+      */
     }
-    Trace("nl-ext-debug") << "computed " << (index == 0 ? "M" : "M_A") << "["
-                          << n << "] = " << ret << std::endl;
+    //if (ret.getType().isReal() && !isArithKind(n.getKind())) {
+      // Trace("nl-ext-mv-debug") << ( index==0 ? "M" : "M_A" ) << "[ " << n
+      // << " ] -> " << ret << std::endl;
+      //may involve transcendental functions
+      //Assert(ret.isConst());
+    //}
+    Trace("nl-ext-mv-debug") << "computed " << (index == 0 ? "M" : "M_A") << "["
+                             << n << "] = " << ret << std::endl;
     d_mv[index][n] = ret;
     return ret;
   }
@@ -898,6 +908,16 @@ Node NonlinearExtension::mkAbs(Node a) {
   }
 }
 
+Node NonlinearExtension::mkValidPhase(Node a, Node pi) {
+  return mkBounded( NodeManager::currentNM()->mkNode( kind::MULT, mkRationalNode(-1), pi ), a, pi );
+}
+
+Node NonlinearExtension::mkBounded( Node l, Node a, Node u ) {
+  return NodeManager::currentNM()->mkNode( kind::AND, 
+           NodeManager::currentNM()->mkNode( kind::GEQ, a, l ),
+           NodeManager::currentNM()->mkNode( kind::LEQ, a, u ) );
+}
+
 // by a <k1> b, a <k2> b, we know a <ret> b
 Kind NonlinearExtension::joinKinds(Kind k1, Kind k2) {
   if (k2 < k1) {
@@ -956,6 +976,11 @@ Kind NonlinearExtension::transKinds(Kind k1, Kind k2) {
   }
 }
 
+bool NonlinearExtension::isTranscendentalKind(Kind k) {
+  Assert( k != kind::TANGENT && k != kind::COSINE ); //eliminated
+  return k==kind::EXPONENTIAL || k==kind::SINE || k==kind::PI;
+}
+ 
 Node NonlinearExtension::mkMonomialRemFactor(
     Node n, const NodeMultiset& n_exp_rem) const {
   std::vector<Node> children;
@@ -1033,27 +1058,26 @@ std::set<Node> NonlinearExtension::getFalseInModel(
   std::set<Node> false_asserts;
   for (size_t i = 0; i < assertions.size(); ++i) {
     Node lit = assertions[i];
-    Node litv = computeModelValue(lit);
-    Trace("nl-ext-mv") << "M[[ " << lit << " ]] -> " << litv;
-    if (litv != d_true) {
-      Trace("nl-ext-mv") << " [model-false]" << std::endl;
-      Assert(litv == d_false);
-      false_asserts.insert(lit);
-    } else {
-      Trace("nl-ext-mv") << std::endl;
+    Node atom = lit.getKind()==NOT ? lit[0] : lit;
+    if( d_skolem_atoms.find( atom )==d_skolem_atoms.end() ){
+      Node litv = computeModelValue(lit);
+      Trace("nl-ext-mv") << "M[[ " << lit << " ]] -> " << litv;
+      if (litv != d_true) {
+        Trace("nl-ext-mv") << " [model-false]" << std::endl;
+        //Assert(litv == d_false);
+        false_asserts.insert(lit);
+      } else {
+        Trace("nl-ext-mv") << std::endl;
+      }
     }
   }
   return false_asserts;
 }
 
-std::vector<Node> NonlinearExtension::splitOnZeros(
-    const std::vector<Node>& ms_vars) {
+std::vector<Node> NonlinearExtension::checkSplitZero() {
   std::vector<Node> lemmas;
-  if (!options::nlExtSplitZero()) {
-    return lemmas;
-  }
-  for (unsigned i = 0; i < ms_vars.size(); i++) {
-    Node v = ms_vars[i];
+  for (unsigned i = 0; i < d_ms_vars.size(); i++) {
+    Node v = d_ms_vars[i];
     if (d_zero_split.insert(v)) {
       Node lem = v.eqNode(d_zero);
       lem = Rewriter::rewrite(lem);
@@ -1067,50 +1091,123 @@ std::vector<Node> NonlinearExtension::splitOnZeros(
 }
 
 void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
-                                       const std::set<Node>& false_asserts) {
-  // processed monomials
-  std::map<Node, bool> ms_proc;
-
-  // list of monomials
-  std::vector<Node> ms;
-  d_containing.getExtTheory()->getTerms(ms);
-  // list of variables occurring in monomials
-  std::vector<Node> ms_vars;
-
-  // register monomials
-  Trace("nl-ext-mv") << "Monomials : " << std::endl;
-  for (unsigned j = 0; j < ms.size(); j++) {
-    Node a = ms[j];
-    registerMonomial(a);
+                                       const std::set<Node>& false_asserts,
+                                       const std::vector<Node>& xts) {
+  d_ms_vars.clear();
+  d_ms_proc.clear();
+  d_ms.clear();
+  d_mterms.clear();
+  d_m_nconst_factor.clear();
+  d_tplane_refine_dir.clear();
+  d_ci.clear();
+  d_ci_exp.clear();
+  d_ci_max.clear();
+  d_tf_rep_map.clear();
+  
+  int lemmas_proc = 0;
+  std::vector<Node> lemmas;  
+  
+  Trace("nl-ext-mv") << "Extended terms : " << std::endl;
+  // register the extended function terms
+  std::map< Node, Node > mvarg_to_term;
+  for( unsigned i=0; i<xts.size(); i++ ){
+    Node a = xts[i];
     computeModelValue(a, 0);
     computeModelValue(a, 1);
-    Assert(d_mv[1][a].isConst());
-    Assert(d_mv[0][a].isConst());
-    Trace("nl-ext-mv") << "  " << a << " -> " << d_mv[1][a] << " ["
-                       << d_mv[0][a] << "]" << std::endl;
-
-    std::map<Node, std::vector<Node> >::iterator itvl = d_m_vlist.find(a);
-    Assert(itvl != d_m_vlist.end());
-    for (unsigned k = 0; k < itvl->second.size(); k++) {
-      if (!IsInVector(ms_vars, itvl->second[k])) {
-        ms_vars.push_back(itvl->second[k]);
+    Trace("nl-ext-mv") << "  " << a << " -> " << d_mv[1][a] << " [actual: "
+                       << d_mv[0][a] << " ]" << std::endl;
+    //Assert(d_mv[1][a].isConst());
+    //Assert(d_mv[0][a].isConst());
+  
+    if( a.getKind()==kind::NONLINEAR_MULT ){
+      d_ms.push_back( a );
+      
+      //context-independent registration
+      registerMonomial(a);
+
+      std::map<Node, std::vector<Node> >::iterator itvl = d_m_vlist.find(a);
+      Assert(itvl != d_m_vlist.end());
+      for (unsigned k = 0; k < itvl->second.size(); k++) {
+        if (!IsInVector(d_ms_vars, itvl->second[k])) {
+          d_ms_vars.push_back(itvl->second[k]);
+        }
+        Node mvk = computeModelValue( itvl->second[k], 1 );
+        if( !mvk.isConst() ){
+          d_m_nconst_factor[a] = true;
+        }
       }
-    }
-    /*
-    //mark processed if has a "one" factor (will look at reduced monomial)
-    std::map< Node, std::map< Node, unsigned > >::iterator itme =
-    d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< Node,
-    unsigned >::iterator itme2 = itme->second.begin(); itme2 !=
-    itme->second.end(); ++itme2 ){ Node v = itme->first; Assert(
-    d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if(
-    mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true;
-    Trace("nl-ext-mv")
-    << "...mark " << a << " reduced since has 1 factor." << std::endl;
-        break;
+      /*
+      //mark processed if has a "one" factor (will look at reduced monomial)
+      std::map< Node, std::map< Node, unsigned > >::iterator itme =
+      d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< Node,
+      unsigned >::iterator itme2 = itme->second.begin(); itme2 !=
+      itme->second.end(); ++itme2 ){ Node v = itme->first; Assert(
+      d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if(
+      mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true;
+      Trace("nl-ext-mv")
+      << "...mark " << a << " reduced since has 1 factor." << std::endl;
+          break;
+        }
+      }
+      */
+    }else if( a.getNumChildren()==1 ){
+      bool consider = true;
+      // get shifted version
+      if( a.getKind()==kind::SINE ){
+        if( d_trig_is_base.find( a )==d_trig_is_base.end() ){
+          consider = false;
+          if( d_trig_base.find( a )==d_trig_base.end() ){
+            Node y = NodeManager::currentNM()->mkSkolem("y",NodeManager::currentNM()->realType(),"phase shifted trigonometric arg");
+            Node new_a = NodeManager::currentNM()->mkNode( a.getKind(), y );
+            d_trig_is_base[new_a] = true;
+            d_trig_base[a] = new_a;
+            Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl;
+            if( d_pi.isNull() ){
+              mkPi();
+              getCurrentPiBounds( lemmas );
+            }
+            Node shift = NodeManager::currentNM()->mkSkolem( "s", NodeManager::currentNM()->integerType(), "number of shifts" );
+            Node shift_lem = NodeManager::currentNM()->mkNode( kind::AND, mkValidPhase( y, d_pi ),
+                               a[0].eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, y, 
+                                              NodeManager::currentNM()->mkNode( kind::MULT, NodeManager::currentNM()->mkConst( Rational(2) ), shift, d_pi ) ) ),
+                               //particular case of above for shift=0
+                               NodeManager::currentNM()->mkNode( kind::IMPLIES, mkValidPhase( a[0], d_pi ), a[0].eqNode( y ) ),
+                               new_a.eqNode( a ) );
+            //must do preprocess on this one
+            Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : shift : " << shift_lem << std::endl;
+            d_containing.getOutputChannel().lemma(shift_lem, false, true);
+            lemmas_proc++;
+          }
+        }
       }
+      if( consider ){
+        Node r = d_containing.getValuation().getModel()->getRepresentative(a[0]);
+        std::map< Node, Node >::iterator itrm = d_tf_rep_map[a.getKind()].find( r );
+        if( itrm!=d_tf_rep_map[a.getKind()].end() ){
+          //verify they have the same model value
+          if( d_mv[1][a]!=d_mv[1][itrm->second] ){
+            //congruence lemma
+            Node cong_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, a[0].eqNode( itrm->second[0] ), a.eqNode( itrm->second ) );
+            lemmas.push_back( cong_lemma );
+            //Assert( false );
+          }
+        }else{
+          d_tf_rep_map[a.getKind()][r] = a;
+        }
+      }
+    }else if( a.getKind()==kind::PI ){
+      //TODO?
+    }else{
+      Assert( false );
     }
-    */
   }
+  
+  lemmas_proc = flushLemmas(lemmas);
+  if (lemmas_proc > 0) {
+    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas during registration." << std::endl;
+    return;
+  }
+
 
   // register constants
   registerMonomial(d_one);
@@ -1120,471 +1217,92 @@ void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     computeModelValue(c, 1);
   }
 
-  int lemmas_proc;
-  std::vector<Node> lemmas;
-
   // register variables
-  Trace("nl-ext-mv") << "Variables : " << std::endl;
-  Trace("nl-ext") << "Get zero split lemmas..." << std::endl;
-  for (unsigned i = 0; i < ms_vars.size(); i++) {
-    Node v = ms_vars[i];
+  Trace("nl-ext-mv") << "Variables in monomials : " << std::endl;
+  for (unsigned i = 0; i < d_ms_vars.size(); i++) {
+    Node v = d_ms_vars[i];
     registerMonomial(v);
     computeModelValue(v, 0);
     computeModelValue(v, 1);
-    Trace("nl-ext-mv") << "  " << v << " -> " << d_mv[0][v] << std::endl;
+    Trace("nl-ext-mv") << "  " << v << " -> " << d_mv[1][v] << " [actual: " << d_mv[0][v] << " ]" << std::endl;
   }
 
-  // possibly split on zero?
-  lemmas = splitOnZeros(ms_vars);
+  //----------------------------------- possibly split on zero
+  if (options::nlExtSplitZero()) {
+    Trace("nl-ext") << "Get zero split lemmas..." << std::endl;
+    lemmas = checkSplitZero();
+    lemmas_proc = flushLemmas(lemmas);
+    if (lemmas_proc > 0) {
+      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
+      return;
+    }
+  }
+
+  //-----------------------------------initial lemmas for transcendental functions
+  lemmas = checkTranscendentalInitialRefine();
   lemmas_proc = flushLemmas(lemmas);
   if (lemmas_proc > 0) {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas."
-                    << std::endl;
+    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
     return;
   }
-
+  
   //-----------------------------------lemmas based on sign (comparison to zero)
-  std::map<Node, int> signs;
-  Trace("nl-ext") << "Get sign lemmas..." << std::endl;
-  for (unsigned j = 0; j < ms.size(); j++) {
-    Node a = ms[j];
-    if (ms_proc.find(a) == ms_proc.end()) {
-      std::vector<Node> exp;
-      Trace("nl-ext-debug") << "  process " << a << "..." << std::endl;
-      signs[a] = compareSign(a, a, 0, 1, exp, lemmas);
-      if (signs[a] == 0) {
-        ms_proc[a] = true;
-        Trace("nl-ext-mv") << "...mark " << a
-                           << " reduced since its value is 0." << std::endl;
-      }
-    }
+  lemmas = checkMonomialSign();
+  lemmas_proc = flushLemmas(lemmas);
+  if (lemmas_proc > 0) {
+    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
+    return;
   }
+  
+  //-----------------------------------monotonicity of transdental functions
+  lemmas = checkTranscendentalMonotonic();
   lemmas_proc = flushLemmas(lemmas);
   if (lemmas_proc > 0) {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas."
-                    << std::endl;
+    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
     return;
   }
 
-  //-----------------------------lemmas based on magnitude of non-zero monomials
-  for (unsigned r = 1; r <= 1; r++) {
-    assignOrderIds(ms_vars, d_order_vars[r], r);
-
-    // sort individual variable lists
-    SortNonlinearExtension smv;
-    smv.d_nla = this;
-    smv.d_order_type = r;
-    smv.d_reverse_order = true;
-    for (unsigned j = 0; j < ms.size(); j++) {
-      std::sort(d_m_vlist[ms[j]].begin(), d_m_vlist[ms[j]].end(), smv);
-    }
-    for (unsigned c = 0; c < 3; c++) {
-      // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L
-      // in lemmas
-      std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers;
-      Trace("nl-ext") << "Get comparison lemmas (order=" << r
-                      << ", compare=" << c << ")..." << std::endl;
-      for (unsigned j = 0; j < ms.size(); j++) {
-        Node a = ms[j];
-        if (ms_proc.find(a) == ms_proc.end()) {
-          if (c == 0) {
-            // compare magnitude against 1
-            std::vector<Node> exp;
-            NodeMultiset a_exp_proc;
-            NodeMultiset b_exp_proc;
-            compareMonomial(a, a, a_exp_proc, d_one, d_one, b_exp_proc, exp,
-                            lemmas, cmp_infers);
-          } else {
-            std::map<Node, NodeMultiset>::iterator itmea = d_m_exp.find(a);
-            Assert(itmea != d_m_exp.end());
-            if (c == 1) {
-              // TODO : not just against containing variables?
-              // compare magnitude against variables
-              for (unsigned k = 0; k < ms_vars.size(); k++) {
-                Node v = ms_vars[k];
-                std::vector<Node> exp;
-                NodeMultiset a_exp_proc;
-                NodeMultiset b_exp_proc;
-                if (itmea->second.find(v) != itmea->second.end()) {
-                  a_exp_proc[v] = 1;
-                  b_exp_proc[v] = 1;
-                  setMonomialFactor(a, v, a_exp_proc);
-                  setMonomialFactor(v, a, b_exp_proc);
-                  compareMonomial(a, a, a_exp_proc, v, v, b_exp_proc, exp,
-                                  lemmas, cmp_infers);
-                }
-              }
-            } else {
-              // compare magnitude against other non-linear monomials
-              for (unsigned k = (j + 1); k < ms.size(); k++) {
-                Node b = ms[k];
-                //(signs[a]==signs[b])==(r==0)
-                if (ms_proc.find(b) == ms_proc.end()) {
-                  std::map<Node, NodeMultiset>::iterator itmeb =
-                      d_m_exp.find(b);
-                  Assert(itmeb != d_m_exp.end());
-
-                  std::vector<Node> exp;
-                  // take common factors of monomials, set minimum of
-                  // common exponents as processed
-                  NodeMultiset a_exp_proc;
-                  NodeMultiset b_exp_proc;
-                  for (NodeMultiset::iterator itmea2 = itmea->second.begin();
-                       itmea2 != itmea->second.end(); ++itmea2) {
-                    NodeMultiset::iterator itmeb2 =
-                        itmeb->second.find(itmea2->first);
-                    if (itmeb2 != itmeb->second.end()) {
-                      unsigned min_exp = itmea2->second > itmeb2->second
-                                             ? itmeb2->second
-                                             : itmea2->second;
-                      a_exp_proc[itmea2->first] = min_exp;
-                      b_exp_proc[itmea2->first] = min_exp;
-                      Trace("nl-ext-comp")
-                          << "Common exponent : " << itmea2->first << " : "
-                          << min_exp << std::endl;
-                    }
-                  }
-                  if (!a_exp_proc.empty()) {
-                    setMonomialFactor(a, b, a_exp_proc);
-                    setMonomialFactor(b, a, b_exp_proc);
-                  }
-                  /*
-                  if( !a_exp_proc.empty() ){
-                    //reduction based on common exponents a > 0 => ( a * b
-                  <> a * c <=> b <> c ), a < 0 => ( a * b <> a * c <=> b
-                  !<> c )  ? }else{ compareMonomial( a, a, a_exp_proc, b,
-                  b, b_exp_proc, exp, lemmas );
-                  }
-                  */
-                  compareMonomial(a, a, a_exp_proc, b, b, b_exp_proc, exp,
-                                  lemmas, cmp_infers);
-                }
-              }
-            }
-          }
-        }
-      }
-      // remove redundant lemmas, e.g. if a > b, b > c, a > c were
-      // inferred, discard lemma with conclusion a > c
-      Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size()
-                           << " lemmas." << std::endl;
-      // naive
-      std::vector<Node> r_lemmas;
-      for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb =
-               cmp_infers.begin();
-           itb != cmp_infers.end(); ++itb) {
-        for (std::map<Node, std::map<Node, Node> >::iterator itc =
-                 itb->second.begin();
-             itc != itb->second.end(); ++itc) {
-          for (std::map<Node, Node>::iterator itc2 = itc->second.begin();
-               itc2 != itc->second.end(); ++itc2) {
-            std::map<Node, bool> visited;
-            for (std::map<Node, Node>::iterator itc3 = itc->second.begin();
-                 itc3 != itc->second.end(); ++itc3) {
-              if (itc3->first != itc2->first) {
-                std::vector<Node> exp;
-                if (cmp_holds(itc3->first, itc2->first, itb->second, exp,
-                              visited)) {
-                  r_lemmas.push_back(itc2->second);
-                  Trace("nl-ext-comp")
-                      << "...inference of " << itc->first << " > "
-                      << itc2->first << " was redundant." << std::endl;
-                  break;
-                }
-              }
-            }
-          }
-        }
-      }
-      std::vector<Node> nr_lemmas;
-      for (unsigned i = 0; i < lemmas.size(); i++) {
-        if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i]) ==
-            r_lemmas.end()) {
-          nr_lemmas.push_back(lemmas[i]);
-        }
-      }
-      // TODO: only take maximal lower/minimial lower bounds?
+  //-----------------------------------lemmas based on magnitude of non-zero monomials
+  Trace("nl-ext-proc") << "Assign order ids..." << std::endl;
+  unsigned r = 3;
+  assignOrderIds(d_ms_vars, d_order_vars, r);
 
-      Trace("nl-ext-comp") << nr_lemmas.size() << " / " << lemmas.size()
-                           << " were non-redundant." << std::endl;
-      lemmas_proc = flushLemmas(nr_lemmas);
-      if (lemmas_proc > 0) {
-        Trace("nl-ext") << "  ...finished with " << lemmas_proc
-                        << " new lemmas (out of possible " << lemmas.size()
-                        << ")." << std::endl;
-        return;
-      }
+  // sort individual variable lists
+  Trace("nl-ext-proc") << "Assign order var lists..." << std::endl;
+  SortNonlinearExtension smv;
+  smv.d_nla = this;
+  smv.d_order_type = r;
+  smv.d_reverse_order = true;
+  for (unsigned j = 0; j < d_ms.size(); j++) {
+    std::sort(d_m_vlist[d_ms[j]].begin(), d_m_vlist[d_ms[j]].end(), smv);
+  }
+  for (unsigned c = 0; c < 3; c++) {
+    // c is effort level
+    lemmas = checkMonomialMagnitude( c );
+    lemmas_proc = flushLemmas(lemmas);
+    if (lemmas_proc > 0) {
+      Trace("nl-ext") << "  ...finished with " << lemmas_proc
+                      << " new lemmas (out of possible " << lemmas.size()
+                      << ")." << std::endl;
+      return;
     }
   }
 
   // sort monomials by degree
+  Trace("nl-ext-proc") << "Sort monomials by degree..." << std::endl;
   SortNonlinearExtension snlad;
   snlad.d_nla = this;
   snlad.d_order_type = 4;
   snlad.d_reverse_order = false;
-  std::sort(ms.begin(), ms.end(), snlad);
+  std::sort(d_ms.begin(), d_ms.end(), snlad);
   // all monomials
-  std::vector<Node> terms;
-  terms.insert(terms.end(), ms_vars.begin(), ms_vars.end());
-  terms.insert(terms.end(), ms.begin(), ms.end());
-
-  // term -> coeff -> rhs -> ( status, exp, b ),
-  //   where we have that : exp =>  ( coeff * term <status> rhs )
-  //   b is true if degree( term ) >= degree( rhs )
-  std::map<Node, std::map<Node, std::map<Node, Kind> > > ci;
-  std::map<Node, std::map<Node, std::map<Node, Node> > > ci_exp;
-  std::map<Node, std::map<Node, std::map<Node, bool> > > ci_max;
-
-  // If ( m, p1, true ), then it would help satisfiability if m were ( >
-  // if p1=true, < if p1=false )
-  std::map<Node, std::map<bool, bool> > tplane_refine_dir;
-
-  // register constraints
-  Trace("nl-ext-debug") << "Register bound constraints..." << std::endl;
-  for (context::CDList<Assertion>::const_iterator it =
-           d_containing.facts_begin();
-       it != d_containing.facts_end(); ++it) {
-    Node lit = (*it).assertion;
-    bool polarity = lit.getKind() != kind::NOT;
-    Node atom = lit.getKind() == kind::NOT ? lit[0] : lit;
-    registerConstraint(atom);
-    bool is_false_lit = false_asserts.find(lit) != false_asserts.end();
-    // add information about bounds to variables
-    std::map<Node, std::map<Node, ConstraintInfo> >::iterator itc =
-        d_c_info.find(atom);
-    std::map<Node, std::map<Node, bool> >::iterator itcm =
-        d_c_info_maxm.find(atom);
-    if (itc != d_c_info.end()) {
-      Assert(itcm != d_c_info_maxm.end());
-      for (std::map<Node, ConstraintInfo>::iterator itcc = itc->second.begin();
-           itcc != itc->second.end(); ++itcc) {
-        Node x = itcc->first;
-        Node coeff = itcc->second.d_coeff;
-        Node rhs = itcc->second.d_rhs;
-        Kind type = itcc->second.d_type;
-        Node exp = lit;
-        if (!polarity) {
-          // reverse
-          if (type == kind::EQUAL) {
-            // we will take the strict inequality in the direction of the
-            // model
-            Node lhs = QuantArith::mkCoeffTerm(coeff, x);
-            Node query = NodeManager::currentNM()->mkNode(kind::GT, lhs, rhs);
-            Node query_mv = computeModelValue(query, 1);
-            if (query_mv == d_true) {
-              exp = query;
-              type = kind::GT;
-            } else {
-              Assert(query_mv == d_false);
-              exp = NodeManager::currentNM()->mkNode(kind::LT, lhs, rhs);
-              type = kind::LT;
-            }
-          } else {
-            type = negateKind(type);
-          }
-        }
-        // add to status if maximal degree
-        ci_max[x][coeff][rhs] = itcm->second.find(x) != itcm->second.end();
-        if (Trace.isOn("nl-ext-bound-debug2")) {
-          Node t = QuantArith::mkCoeffTerm(coeff, x);
-          Trace("nl-ext-bound-debug2")
-              << "Add Bound: " << t << " " << type << " " << rhs << " by "
-              << exp << std::endl;
-        }
-        bool updated = true;
-        std::map<Node, Kind>::iterator its = ci[x][coeff].find(rhs);
-        if (its == ci[x][coeff].end()) {
-          ci[x][coeff][rhs] = type;
-          ci_exp[x][coeff][rhs] = exp;
-        } else if (type != its->second) {
-          Trace("nl-ext-bound-debug2")
-              << "Joining kinds : " << type << " " << its->second << std::endl;
-          Kind jk = joinKinds(type, its->second);
-          if (jk == kind::UNDEFINED_KIND) {
-            updated = false;
-          } else if (jk != its->second) {
-            if (jk == type) {
-              ci[x][coeff][rhs] = type;
-              ci_exp[x][coeff][rhs] = exp;
-            } else {
-              ci[x][coeff][rhs] = jk;
-              ci_exp[x][coeff][rhs] = NodeManager::currentNM()->mkNode(
-                  kind::AND, ci_exp[x][coeff][rhs], exp);
-            }
-          } else {
-            updated = false;
-          }
-        }
-        if (Trace.isOn("nl-ext-bound")) {
-          if (updated) {
-            Trace("nl-ext-bound") << "Bound: ";
-            debugPrintBound("nl-ext-bound", coeff, x, ci[x][coeff][rhs], rhs);
-            Trace("nl-ext-bound") << " by " << ci_exp[x][coeff][rhs];
-            if (ci_max[x][coeff][rhs]) {
-              Trace("nl-ext-bound") << ", is max degree";
-            }
-            Trace("nl-ext-bound") << std::endl;
-          }
-        }
-        // compute if bound is not satisfied, and store what is required
-        // for a possible refinement
-        if (options::nlExtTangentPlanes()) {
-          if (is_false_lit) {
-            Node rhs_v = computeModelValue(rhs, 0);
-            Node x_v = computeModelValue(x, 0);
-            bool needsRefine = false;
-            bool refineDir;
-            if (rhs_v == x_v) {
-              if (type == kind::GT) {
-                needsRefine = true;
-                refineDir = true;
-              } else if (type == kind::LT) {
-                needsRefine = true;
-                refineDir = false;
-              }
-            } else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) {
-              if (type != kind::GT && type != kind::GEQ) {
-                needsRefine = true;
-                refineDir = false;
-              }
-            } else {
-              if (type != kind::LT && type != kind::LEQ) {
-                needsRefine = true;
-                refineDir = true;
-              }
-            }
-            Trace("nl-ext-tplanes-cons-debug")
-                << "...compute if bound corresponds to a required "
-                   "refinement"
-                << std::endl;
-            Trace("nl-ext-tplanes-cons-debug")
-                << "...M[" << x << "] = " << x_v << ", M[" << rhs
-                << "] = " << rhs_v << std::endl;
-            Trace("nl-ext-tplanes-cons-debug") << "...refine = " << needsRefine
-                                               << "/" << refineDir << std::endl;
-            if (needsRefine) {
-              Trace("nl-ext-tplanes-cons")
-                  << "---> By " << lit << " and since M[" << x << "] = " << x_v
-                  << ", M[" << rhs << "] = " << rhs_v << ", ";
-              Trace("nl-ext-tplanes-cons")
-                  << "monomial " << x << " should be "
-                  << (refineDir ? "larger" : "smaller") << std::endl;
-              tplane_refine_dir[x][refineDir] = true;
-            }
-          }
-        }
-      }
-    }
-  }
-  // reflexive constraints
-  Node null_coeff;
-  for (unsigned j = 0; j < terms.size(); j++) {
-    Node n = terms[j];
-    ci[n][null_coeff][n] = kind::EQUAL;
-    ci_exp[n][null_coeff][n] = d_true;
-    ci_max[n][null_coeff][n] = false;
-  }
+  d_mterms.insert(d_mterms.end(), d_ms_vars.begin(), d_ms_vars.end());
+  d_mterms.insert(d_mterms.end(), d_ms.begin(), d_ms.end());
 
-  //-----------------------------------------------------------------------------------------inferred
-  // bounds lemmas, e.g. x >= t => y*x >= y*t
-  Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl;
-
-  std::vector<Node> nt_lemmas;
-  for (unsigned k = 0; k < terms.size(); k++) {
-    Node x = terms[k];
-    Trace("nl-ext-bound-debug")
-        << "Process bounds for " << x << " : " << std::endl;
-    std::map<Node, std::vector<Node> >::iterator itm =
-        d_m_contain_parent.find(x);
-    if (itm != d_m_contain_parent.end()) {
-      Trace("nl-ext-bound-debug") << "...has " << itm->second.size()
-                                  << " parent monomials." << std::endl;
-      // check derived bounds
-      std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc =
-          ci.find(x);
-      if (itc != ci.end()) {
-        for (std::map<Node, std::map<Node, Kind> >::iterator itcc =
-                 itc->second.begin();
-             itcc != itc->second.end(); ++itcc) {
-          Node coeff = itcc->first;
-          Node t = QuantArith::mkCoeffTerm(coeff, x);
-          for (std::map<Node, Kind>::iterator itcr = itcc->second.begin();
-               itcr != itcc->second.end(); ++itcr) {
-            Node rhs = itcr->first;
-            // only consider this bound if maximal degree
-            if (ci_max[x][coeff][rhs]) {
-              Kind type = itcr->second;
-              for (unsigned j = 0; j < itm->second.size(); j++) {
-                Node y = itm->second[j];
-                Assert(d_m_contain_mult[x].find(y) !=
-                       d_m_contain_mult[x].end());
-                Node mult = d_m_contain_mult[x][y];
-                // x <k> t => m*x <k'> t  where y = m*x
-                // get the sign of mult
-                Node mmv = computeModelValue(mult);
-                Trace("nl-ext-bound-debug2")
-                    << "Model value of " << mult << " is " << mmv << std::endl;
-                Assert(mmv.isConst());
-                int mmv_sign = mmv.getConst<Rational>().sgn();
-                Trace("nl-ext-bound-debug2")
-                    << "  sign of " << mmv << " is " << mmv_sign << std::endl;
-                if (mmv_sign != 0) {
-                  Trace("nl-ext-bound-debug")
-                      << "  from " << x << " * " << mult << " = " << y
-                      << " and " << t << " " << type << " " << rhs
-                      << ", infer : " << std::endl;
-                  Kind infer_type =
-                      mmv_sign == -1 ? reverseRelationKind(type) : type;
-                  Node infer_lhs =
-                      NodeManager::currentNM()->mkNode(kind::MULT, mult, t);
-                  Node infer_rhs =
-                      NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs);
-                  Node infer = NodeManager::currentNM()->mkNode(
-                      infer_type, infer_lhs, infer_rhs);
-                  Trace("nl-ext-bound-debug") << "     " << infer << std::endl;
-                  infer = Rewriter::rewrite(infer);
-                  Trace("nl-ext-bound-debug2")
-                      << "     ...rewritten : " << infer << std::endl;
-                  // check whether it is false in model for abstraction
-                  Node infer_mv = computeModelValue(infer, 1);
-                  Trace("nl-ext-bound-debug")
-                      << "       ...infer model value is " << infer_mv
-                      << std::endl;
-                  if (infer_mv == d_false) {
-                    Node exp = NodeManager::currentNM()->mkNode(
-                        kind::AND,
-                        NodeManager::currentNM()->mkNode(
-                            mmv_sign == 1 ? kind::GT : kind::LT, mult, d_zero),
-                        ci_exp[x][coeff][rhs]);
-                    Node iblem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
-                                                                  exp, infer);
-                    Node pr_iblem = iblem;
-                    iblem = Rewriter::rewrite(iblem);
-                    bool introNewTerms = hasNewMonomials(iblem, ms);
-                    Trace("nl-ext-bound-lemma")
-                        << "*** Bound inference lemma : " << iblem
-                        << " (pre-rewrite : " << pr_iblem << ")" << std::endl;
-                    // Trace("nl-ext-bound-lemma") << "       intro new
-                    // monomials = " << introNewTerms << std::endl;
-                    if (!introNewTerms) {
-                      lemmas.push_back(iblem);
-                    } else {
-                      nt_lemmas.push_back(iblem);
-                    }
-                  }
-                } else {
-                  Trace("nl-ext-bound-debug") << "     ...coefficient " << mult
-                                              << " is zero." << std::endl;
-                }
-              }
-            }
-          }
-        }
-      }
-    } else {
-      Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl;
-    }
-  }
+  //-----------------------------------inferred bounds lemmas
+  //  e.g. x >= t => y*x >= y*t
+  std::vector< Node > nt_lemmas;
+  lemmas = checkMonomialInferBounds( nt_lemmas, false_asserts );
   // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
   // nt_lemmas.size() << std::endl;  prioritize lemmas that do not
   // introduce new monomials
@@ -1594,226 +1312,43 @@ void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                     << std::endl;
     return;
   }
-
-  //------------------------------------resolution bound inferences, e.g.
-  //(
-  // y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
-  if (options::nlExtResBound()) {
-    Trace("nl-ext") << "Get resolution inferred bound lemmas..." << std::endl;
-    for (unsigned j = 0; j < terms.size(); j++) {
-      Node a = terms[j];
-      std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca =
-          ci.find(a);
-      if (itca != ci.end()) {
-        for (unsigned k = (j + 1); k < terms.size(); k++) {
-          Node b = terms[k];
-          std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator
-              itcb = ci.find(b);
-          if (itcb != ci.end()) {
-            Trace("nl-ext-rbound-debug") << "resolution inferences : compare "
-                                         << a << " and " << b << std::endl;
-            // if they have common factors
-            std::map<Node, Node>::iterator ita = d_mono_diff[a].find(b);
-            if (ita != d_mono_diff[a].end()) {
-              std::map<Node, Node>::iterator itb = d_mono_diff[b].find(a);
-              Assert(itb != d_mono_diff[b].end());
-              Node mv_a = computeModelValue(ita->second, 1);
-              Assert(mv_a.isConst());
-              int mv_a_sgn = mv_a.getConst<Rational>().sgn();
-              Assert(mv_a_sgn != 0);
-              Node mv_b = computeModelValue(itb->second, 1);
-              Assert(mv_b.isConst());
-              int mv_b_sgn = mv_b.getConst<Rational>().sgn();
-              Assert(mv_b_sgn != 0);
-              Trace("nl-ext-rbound") << "Get resolution inferences for [a] "
-                                     << a << " vs [b] " << b << std::endl;
-              Trace("nl-ext-rbound")
-                  << "  [a] factor is " << ita->second
-                  << ", sign in model = " << mv_a_sgn << std::endl;
-              Trace("nl-ext-rbound")
-                  << "  [b] factor is " << itb->second
-                  << ", sign in model = " << mv_b_sgn << std::endl;
-
-              std::vector<Node> exp;
-              // bounds of a
-              for (std::map<Node, std::map<Node, Kind> >::iterator itcac =
-                       itca->second.begin();
-                   itcac != itca->second.end(); ++itcac) {
-                Node coeff_a = itcac->first;
-                for (std::map<Node, Kind>::iterator itcar =
-                         itcac->second.begin();
-                     itcar != itcac->second.end(); ++itcar) {
-                  Node rhs_a = itcar->first;
-                  Node rhs_a_res_base = NodeManager::currentNM()->mkNode(
-                      kind::MULT, itb->second, rhs_a);
-                  rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
-                  if (!hasNewMonomials(rhs_a_res_base, ms)) {
-                    Kind type_a = itcar->second;
-                    exp.push_back(ci_exp[a][coeff_a][rhs_a]);
-
-                    // bounds of b
-                    for (std::map<Node, std::map<Node, Kind> >::iterator itcbc =
-                             itcb->second.begin();
-                         itcbc != itcb->second.end(); ++itcbc) {
-                      Node coeff_b = itcbc->first;
-                      Node rhs_a_res =
-                          QuantArith::mkCoeffTerm(coeff_b, rhs_a_res_base);
-                      for (std::map<Node, Kind>::iterator itcbr =
-                               itcbc->second.begin();
-                           itcbr != itcbc->second.end(); ++itcbr) {
-                        Node rhs_b = itcbr->first;
-                        Node rhs_b_res = NodeManager::currentNM()->mkNode(
-                            kind::MULT, ita->second, rhs_b);
-                        rhs_b_res = QuantArith::mkCoeffTerm(coeff_a, rhs_b_res);
-                        rhs_b_res = Rewriter::rewrite(rhs_b_res);
-                        if (!hasNewMonomials(rhs_b_res, ms)) {
-                          Kind type_b = itcbr->second;
-                          exp.push_back(ci_exp[b][coeff_b][rhs_b]);
-                          if (Trace.isOn("nl-ext-rbound")) {
-                            Trace("nl-ext-rbound") << "* try bounds : ";
-                            debugPrintBound("nl-ext-rbound", coeff_a, a, type_a,
-                                            rhs_a);
-                            Trace("nl-ext-rbound") << std::endl;
-                            Trace("nl-ext-rbound") << "               ";
-                            debugPrintBound("nl-ext-rbound", coeff_b, b, type_b,
-                                            rhs_b);
-                            Trace("nl-ext-rbound") << std::endl;
-                          }
-                          Kind types[2];
-                          for (unsigned r = 0; r < 2; r++) {
-                            Node pivot_factor =
-                                r == 0 ? itb->second : ita->second;
-                            int pivot_factor_sign =
-                                r == 0 ? mv_b_sgn : mv_a_sgn;
-                            types[r] = r == 0 ? type_a : type_b;
-                            if (pivot_factor_sign == (r == 0 ? 1 : -1)) {
-                              types[r] = reverseRelationKind(types[r]);
-                            }
-                            if (pivot_factor_sign == 1) {
-                              exp.push_back(NodeManager::currentNM()->mkNode(
-                                  kind::GT, pivot_factor, d_zero));
-                            } else {
-                              exp.push_back(NodeManager::currentNM()->mkNode(
-                                  kind::LT, pivot_factor, d_zero));
-                            }
-                          }
-                          Kind jk = transKinds(types[0], types[1]);
-                          Trace("nl-ext-rbound-debug")
-                              << "trans kind : " << types[0] << " + "
-                              << types[1] << " = " << jk << std::endl;
-                          if (jk != kind::UNDEFINED_KIND) {
-                            Node conc = NodeManager::currentNM()->mkNode(
-                                jk, rhs_a_res, rhs_b_res);
-                            Node conc_mv = computeModelValue(conc, 1);
-                            if (conc_mv == d_false) {
-                              Node rblem = NodeManager::currentNM()->mkNode(
-                                  kind::IMPLIES,
-                                  NodeManager::currentNM()->mkNode(kind::AND,
-                                                                   exp),
-                                  conc);
-                              Trace("nl-ext-rbound-lemma-debug")
-                                  << "Resolution bound lemma "
-                                     "(pre-rewrite) "
-                                     ": "
-                                  << rblem << std::endl;
-                              rblem = Rewriter::rewrite(rblem);
-                              Trace("nl-ext-rbound-lemma")
-                                  << "Resolution bound lemma : " << rblem
-                                  << std::endl;
-                              lemmas.push_back(rblem);
-                            }
-                          }
-                          exp.pop_back();
-                          exp.pop_back();
-                          exp.pop_back();
-                        }
-                      }
-                    }
-                    exp.pop_back();
-                  }
-                }
-              }
-            }
-          }
-        }
-      }
-    }
-    lemmas_proc = flushLemmas(lemmas);
-    if (lemmas_proc > 0) {
-      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas."
-                      << std::endl;
-      return;
-    }
-  }
-
-  // from inferred bound inferences
+  
+  // from inferred bound inferences : now do ones that introduce new terms
   lemmas_proc = flushLemmas(nt_lemmas);
   if (lemmas_proc > 0) {
     Trace("nl-ext") << "  ...finished with " << lemmas_proc
                     << " new (monomial-introducing) lemmas." << std::endl;
     return;
   }
+  
+  //------------------------------------factoring lemmas
+  //   x*y + x*z >= t => exists k. k = y + z ^ x*k >= t
+  if( options::nlExtFactor() ){
+    lemmas = checkFactoring( false_asserts );
+    lemmas_proc = flushLemmas(lemmas);
+    if (lemmas_proc > 0) {
+      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
+      return;
+    }
+  }
 
-  if (options::nlExtTangentPlanes()) {
-    Trace("nl-ext") << "Get tangent plane lemmas..." << std::endl;
-    unsigned kstart = ms_vars.size();
-    for (unsigned k = kstart; k < terms.size(); k++) {
-      Node t = terms[k];
-      // if this term requires a refinement
-      if (tplane_refine_dir.find(t) != tplane_refine_dir.end()) {
-        Trace("nl-ext-tplanes")
-            << "Look at monomial requiring refinement : " << t << std::endl;
-        // get a decomposition
-        std::map<Node, std::vector<Node> >::iterator it =
-            d_m_contain_children.find(t);
-        if (it != d_m_contain_children.end()) {
-          std::map<Node, std::map<Node, bool> > dproc;
-          for (unsigned j = 0; j < it->second.size(); j++) {
-            Node tc = it->second[j];
-            if (tc != d_one) {
-              Node tc_diff = d_m_contain_umult[tc][t];
-              Assert(!tc_diff.isNull());
-              Node a = tc < tc_diff ? tc : tc_diff;
-              Node b = tc < tc_diff ? tc_diff : tc;
-              if (dproc[a].find(b) == dproc[a].end()) {
-                dproc[a][b] = true;
-                Trace("nl-ext-tplanes")
-                    << "  decomposable into : " << a << " * " << b << std::endl;
-                Node a_v = computeModelValue(a, 1);
-                Node b_v = computeModelValue(b, 1);
-                // tangent plane
-                Node tplane = NodeManager::currentNM()->mkNode(
-                    kind::MINUS,
-                    NodeManager::currentNM()->mkNode(
-                        kind::PLUS,
-                        NodeManager::currentNM()->mkNode(kind::MULT, b_v, a),
-                        NodeManager::currentNM()->mkNode(kind::MULT, a_v, b)),
-                    NodeManager::currentNM()->mkNode(kind::MULT, a_v, b_v));
-                for (unsigned d = 0; d < 4; d++) {
-                  Node aa = NodeManager::currentNM()->mkNode(
-                      d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v);
-                  Node ab = NodeManager::currentNM()->mkNode(
-                      d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v);
-                  Node conc = NodeManager::currentNM()->mkNode(
-                      d <= 1 ? kind::LEQ : kind::GEQ, t, tplane);
-                  Node tlem = NodeManager::currentNM()->mkNode(
-                      kind::OR, aa.negate(), ab.negate(), conc);
-                  Trace("nl-ext-tplanes")
-                      << "Tangent plane lemma : " << tlem << std::endl;
-                  lemmas.push_back(tlem);
-                }
-              }
-            }
-          }
-        }
-      }
+  //------------------------------------resolution bound inferences
+  //  e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
+  if (options::nlExtResBound()) {
+    lemmas = checkMonomialInferResBounds();
+    lemmas_proc = flushLemmas(lemmas);
+    if (lemmas_proc > 0) {
+      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
+      return;
     }
-    Trace("nl-ext") << "...trying " << lemmas.size()
-                    << " tangent plane lemmas..." << std::endl;
+  }
+  
+  //------------------------------------tangent planes
+  if (options::nlExtTangentPlanes()) {
+    lemmas = checkTangentPlanes();
     lemmas_proc = flushLemmas(lemmas);
     if (lemmas_proc > 0) {
-      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas."
-                      << std::endl;
+      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
       return;
     }
   }
@@ -1852,10 +1387,13 @@ void NonlinearExtension::check(Theory::Effort e) {
       const Assertion& assertion = *it;
       assertions.push_back(assertion.assertion);
     }
-    
     const std::set<Node> false_asserts = getFalseInModel(assertions);
+    
+    std::vector<Node> xts;
+    d_containing.getExtTheory()->getTerms(xts);
+    
     if (!false_asserts.empty()) {
-      checkLastCall(assertions, false_asserts);
+      checkLastCall(assertions, false_asserts, xts);
     }else{
       //must ensure that shared terms are equal to their concrete value
       std::vector< Node > lemmas;
@@ -1902,6 +1440,11 @@ void NonlinearExtension::assignOrderIds(std::vector<Node>& vars,
   for (unsigned j = 0; j < vars.size(); j++) {
     Node x = vars[j];
     Node v = get_compare_value(x, orderType);
+    if( !v.isConst() ){
+      Trace("nl-ext-mvo") << "..do not assign order to " << x << " : " << v << std::endl;
+      //don't assign for non-constant values (transcendental function apps)
+      break;
+    }
     Trace("nl-ext-mvo") << "  order " << x << " : " << v << std::endl;
     if (v != prev) {
       // builtin points
@@ -1944,8 +1487,21 @@ void NonlinearExtension::assignOrderIds(std::vector<Node>& vars,
 int NonlinearExtension::compare(Node i, Node j, unsigned orderType) const {
   Assert(orderType >= 0);
   if (orderType <= 3) {
-    return compare_value(get_compare_value(i, orderType),
-                         get_compare_value(j, orderType), orderType);
+    Node ci = get_compare_value(i, orderType);
+    Node cj = get_compare_value(j, orderType);
+    if( ci.isConst() ){
+      if( cj.isConst() ){
+        return compare_value(ci, cj, orderType);
+      }else{
+        return 1; 
+      }
+    }else{
+      if( cj.isConst() ){
+        return -1;
+      }else{
+        return 0;
+      }
+    }
     // minimal degree
   } else if (orderType == 4) {
     unsigned i_count = getCount(d_m_degree, i);
@@ -1956,10 +1512,32 @@ int NonlinearExtension::compare(Node i, Node j, unsigned orderType) const {
   }
 }
 
+
+
+void NonlinearExtension::mkPi(){
+  if( d_pi.isNull() ){
+    d_pi = NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI );
+    d_pi_2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ) );
+    d_pi_neg_2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(-1)/Rational(2) ) ) );
+    d_pi_neg = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(-1) ) ) );
+    //initialize bounds
+    d_pi_bound[0] = NodeManager::currentNM()->mkConst( Rational(333)/Rational(106) );
+    d_pi_bound[1] = NodeManager::currentNM()->mkConst( Rational(355)/Rational(113) );
+  }
+}
+
+void NonlinearExtension::getCurrentPiBounds( std::vector< Node >& lemmas ) {
+  Node pi_lem = NodeManager::currentNM()->mkNode( kind::AND, 
+                  NodeManager::currentNM()->mkNode( kind::GT, d_pi, d_pi_bound[0] ),
+                  NodeManager::currentNM()->mkNode( kind::LT, d_pi, d_pi_bound[1] ) );
+  lemmas.push_back( pi_lem );
+}
+
 int NonlinearExtension::compare_value(Node i, Node j,
                                       unsigned orderType) const {
   Assert(orderType >= 0 && orderType <= 3);
-  Trace("nl-ext-debug") << "compare_value " << i << " " << j
+  Assert( i.isConst() && j.isConst() );
+  Trace("nl-ext-debug") << "compare value " << i << " " << j
                         << ", o = " << orderType << std::endl;
   int ret;
   if (i == j) {
@@ -1991,8 +1569,7 @@ Node NonlinearExtension::get_compare_value(Node i, unsigned orderType) const {
   return iti->second;
 }
 
-// trying to show a <> 0 by inequalities between variables in monomial a w.r.t
-// 0
+// show a <> 0 by inequalities between variables in monomial a w.r.t 0
 int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index,
                                     int status, std::vector<Node>& exp,
                                     std::vector<Node>& lem) {
@@ -2011,8 +1588,9 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index,
     Node av = d_m_vlist[a][a_index];
     unsigned aexp = d_m_exp[a][av];
     // take current sign in model
-    Assert(d_mv[0].find(av) != d_mv[0].end());
-    int sgn = d_mv[0][av].getConst<Rational>().sgn();
+    Assert( d_mv[1].find(av) != d_mv[0].end() );
+    Assert( d_mv[1][av].isConst() );
+    int sgn = d_mv[1][av].getConst<Rational>().sgn();
     Trace("nl-ext-debug") << "Process var " << av << "^" << aexp
                           << ", model sign = " << sgn << std::endl;
     if (sgn == 0) {
@@ -2126,8 +1704,8 @@ bool NonlinearExtension::compareMonomial(
         return compareMonomial(oa, a, a_index + 1, a_exp_proc, ob, b, b_index,
                                b_exp_proc, status, exp, lem, cmp_infers);
       }
-      Assert(d_order_vars[1].find(av) != d_order_vars[1].end());
-      avo = d_order_vars[1][av];
+      Assert(d_order_vars.find(av) != d_order_vars.end());
+      avo = d_order_vars[av];
     }
     Node bv;
     unsigned bexp = 0;
@@ -2140,12 +1718,12 @@ bool NonlinearExtension::compareMonomial(
         return compareMonomial(oa, a, a_index, a_exp_proc, ob, b, b_index + 1,
                                b_exp_proc, status, exp, lem, cmp_infers);
       }
-      Assert(d_order_vars[1].find(bv) != d_order_vars[1].end());
-      bvo = d_order_vars[1][bv];
+      Assert(d_order_vars.find(bv) != d_order_vars.end());
+      bvo = d_order_vars[bv];
     }
     // get "one" information
-    Assert(d_order_vars[1].find(d_one) != d_order_vars[1].end());
-    unsigned ovo = d_order_vars[1][d_one];
+    Assert(d_order_vars.find(d_one) != d_order_vars.end());
+    unsigned ovo = d_order_vars[d_one];
     Trace("nl-ext-comp-debug") << "....vars : " << av << "^" << aexp << " "
                                << bv << "^" << bexp << std::endl;
 
@@ -2266,6 +1844,1024 @@ void NonlinearExtension::MonomialIndex::addTerm(Node n,
   }
 }
 
+std::vector<Node> NonlinearExtension::checkMonomialSign() {
+  std::vector<Node> lemmas;
+  std::map<Node, int> signs;
+  Trace("nl-ext") << "Get monomial sign lemmas..." << std::endl;
+  for (unsigned j = 0; j < d_ms.size(); j++) {
+    Node a = d_ms[j];
+    if (d_ms_proc.find(a) == d_ms_proc.end()) {
+      std::vector<Node> exp;
+      Trace("nl-ext-debug") << "  process " << a << ", mv=" << d_mv[0][a] << "..." << std::endl;
+      if( d_m_nconst_factor.find( a )==d_m_nconst_factor.end() ){
+        signs[a] = compareSign(a, a, 0, 1, exp, lemmas);
+        if (signs[a] == 0) {
+          d_ms_proc[a] = true;
+          Trace("nl-ext-debug") << "...mark " << a
+                             << " reduced since its value is 0." << std::endl;
+        }
+      }else{
+        Trace("nl-ext-debug") << "...can't conclude sign lemma for " << a << " since model value of a factor is non-constant." << std::endl;
+        //TODO
+      }
+    }
+  }
+  return lemmas;
+}
+
+std::vector<Node> NonlinearExtension::checkMonomialMagnitude( unsigned c ) {
+  unsigned r = 1;
+  std::vector<Node> lemmas;
+// if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L
+  // in lemmas
+  std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers;
+  Trace("nl-ext") << "Get monomial comparison lemmas (order=" << r
+                  << ", compare=" << c << ")..." << std::endl;
+  for (unsigned j = 0; j < d_ms.size(); j++) {
+    Node a = d_ms[j];
+    if (d_ms_proc.find(a) == d_ms_proc.end() && 
+        d_m_nconst_factor.find( a )==d_m_nconst_factor.end()) {
+      if (c == 0) {
+        // compare magnitude against 1
+        std::vector<Node> exp;
+        NodeMultiset a_exp_proc;
+        NodeMultiset b_exp_proc;
+        compareMonomial(a, a, a_exp_proc, d_one, d_one, b_exp_proc, exp,
+                        lemmas, cmp_infers);
+      } else {
+        std::map<Node, NodeMultiset>::iterator itmea = d_m_exp.find(a);
+        Assert(itmea != d_m_exp.end());
+        if (c == 1) {
+          // TODO : not just against containing variables?
+          // compare magnitude against variables
+          for (unsigned k = 0; k < d_ms_vars.size(); k++) {
+            Node v = d_ms_vars[k];
+            Assert( d_mv[0].find( v )!=d_mv[0].end() );
+            if( d_mv[0][v].isConst() ){
+              std::vector<Node> exp;
+              NodeMultiset a_exp_proc;
+              NodeMultiset b_exp_proc;
+              if (itmea->second.find(v) != itmea->second.end()) {
+                a_exp_proc[v] = 1;
+                b_exp_proc[v] = 1;
+                setMonomialFactor(a, v, a_exp_proc);
+                setMonomialFactor(v, a, b_exp_proc);
+                compareMonomial(a, a, a_exp_proc, v, v, b_exp_proc, exp,
+                                lemmas, cmp_infers);
+              }
+            }
+          }
+        } else {
+          // compare magnitude against other non-linear monomials
+          for (unsigned k = (j + 1); k < d_ms.size(); k++) {
+            Node b = d_ms[k];
+            //(signs[a]==signs[b])==(r==0)
+            if (d_ms_proc.find(b) == d_ms_proc.end() && 
+                d_m_nconst_factor.find( b )==d_m_nconst_factor.end()) {
+              std::map<Node, NodeMultiset>::iterator itmeb =
+                  d_m_exp.find(b);
+              Assert(itmeb != d_m_exp.end());
+
+              std::vector<Node> exp;
+              // take common factors of monomials, set minimum of
+              // common exponents as processed
+              NodeMultiset a_exp_proc;
+              NodeMultiset b_exp_proc;
+              for (NodeMultiset::iterator itmea2 = itmea->second.begin();
+                   itmea2 != itmea->second.end(); ++itmea2) {
+                NodeMultiset::iterator itmeb2 =
+                    itmeb->second.find(itmea2->first);
+                if (itmeb2 != itmeb->second.end()) {
+                  unsigned min_exp = itmea2->second > itmeb2->second
+                                         ? itmeb2->second
+                                         : itmea2->second;
+                  a_exp_proc[itmea2->first] = min_exp;
+                  b_exp_proc[itmea2->first] = min_exp;
+                  Trace("nl-ext-comp")
+                      << "Common exponent : " << itmea2->first << " : "
+                      << min_exp << std::endl;
+                }
+              }
+              if (!a_exp_proc.empty()) {
+                setMonomialFactor(a, b, a_exp_proc);
+                setMonomialFactor(b, a, b_exp_proc);
+              }
+              /*
+              if( !a_exp_proc.empty() ){
+                //reduction based on common exponents a > 0 => ( a * b
+              <> a * c <=> b <> c ), a < 0 => ( a * b <> a * c <=> b
+              !<> c )  ? }else{ compareMonomial( a, a, a_exp_proc, b,
+              b, b_exp_proc, exp, lemmas );
+              }
+              */
+              compareMonomial(a, a, a_exp_proc, b, b, b_exp_proc, exp,
+                              lemmas, cmp_infers);
+            }
+          }
+        }
+      }
+    }
+  }
+  // remove redundant lemmas, e.g. if a > b, b > c, a > c were
+  // inferred, discard lemma with conclusion a > c
+  Trace("nl-ext-comp") << "Compute redundand_cies for " << lemmas.size()
+                       << " lemmas." << std::endl;
+  // naive
+  std::vector<Node> r_lemmas;
+  for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb =
+           cmp_infers.begin();
+       itb != cmp_infers.end(); ++itb) {
+    for (std::map<Node, std::map<Node, Node> >::iterator itc =
+             itb->second.begin();
+         itc != itb->second.end(); ++itc) {
+      for (std::map<Node, Node>::iterator itc2 = itc->second.begin();
+           itc2 != itc->second.end(); ++itc2) {
+        std::map<Node, bool> visited;
+        for (std::map<Node, Node>::iterator itc3 = itc->second.begin();
+             itc3 != itc->second.end(); ++itc3) {
+          if (itc3->first != itc2->first) {
+            std::vector<Node> exp;
+            if (cmp_holds(itc3->first, itc2->first, itb->second, exp,
+                          visited)) {
+              r_lemmas.push_back(itc2->second);
+              Trace("nl-ext-comp")
+                  << "...inference of " << itc->first << " > "
+                  << itc2->first << " was redundant." << std::endl;
+              break;
+            }
+          }
+        }
+      }
+    }
+  }
+  std::vector<Node> nr_lemmas;
+  for (unsigned i = 0; i < lemmas.size(); i++) {
+    if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i]) ==
+        r_lemmas.end()) {
+      nr_lemmas.push_back(lemmas[i]);
+    }
+  }
+  // TODO: only take maximal lower/minimial lower bounds?
+
+  Trace("nl-ext-comp") << nr_lemmas.size() << " / " << lemmas.size()
+                       << " were non-redundant." << std::endl;
+  return nr_lemmas;
+}
+
+std::vector<Node> NonlinearExtension::checkTangentPlanes() {
+  std::vector< Node > lemmas;
+  Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl;
+  unsigned kstart = d_ms_vars.size();
+  for (unsigned k = kstart; k < d_mterms.size(); k++) {
+    Node t = d_mterms[k];
+    // if this term requires a refinement
+    if (d_tplane_refine_dir.find(t) != d_tplane_refine_dir.end()) {
+      Trace("nl-ext-tplanes")
+          << "Look at monomial requiring refinement : " << t << std::endl;
+      // get a decomposition
+      std::map<Node, std::vector<Node> >::iterator it =
+          d_m_contain_children.find(t);
+      if (it != d_m_contain_children.end()) {
+        std::map<Node, std::map<Node, bool> > dproc;
+        for (unsigned j = 0; j < it->second.size(); j++) {
+          Node tc = it->second[j];
+          if (tc != d_one) {
+            Node tc_diff = d_m_contain_umult[tc][t];
+            Assert(!tc_diff.isNull());
+            Node a = tc < tc_diff ? tc : tc_diff;
+            Node b = tc < tc_diff ? tc_diff : tc;
+            if (dproc[a].find(b) == dproc[a].end()) {
+              dproc[a][b] = true;
+              Trace("nl-ext-tplanes")
+                  << "  decomposable into : " << a << " * " << b << std::endl;
+              Node a_v = computeModelValue(a, 1);
+              Node b_v = computeModelValue(b, 1);
+              // tangent plane
+              Node tplane = NodeManager::currentNM()->mkNode(
+                  kind::MINUS,
+                  NodeManager::currentNM()->mkNode(
+                      kind::PLUS,
+                      NodeManager::currentNM()->mkNode(kind::MULT, b_v, a),
+                      NodeManager::currentNM()->mkNode(kind::MULT, a_v, b)),
+                  NodeManager::currentNM()->mkNode(kind::MULT, a_v, b_v));
+              for (unsigned d = 0; d < 4; d++) {
+                Node aa = NodeManager::currentNM()->mkNode(
+                    d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v);
+                Node ab = NodeManager::currentNM()->mkNode(
+                    d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v);
+                Node conc = NodeManager::currentNM()->mkNode(
+                    d <= 1 ? kind::LEQ : kind::GEQ, t, tplane);
+                Node tlem = NodeManager::currentNM()->mkNode(
+                    kind::OR, aa.negate(), ab.negate(), conc);
+                Trace("nl-ext-tplanes")
+                    << "Tangent plane lemma : " << tlem << std::endl;
+                lemmas.push_back(tlem);
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  Trace("nl-ext") << "...trying " << lemmas.size()
+                  << " tangent plane lemmas..." << std::endl;
+  return lemmas;
+}              
+                    
+
+                    
+std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node>& nt_lemmas,
+                                                                const std::set<Node>& false_asserts ) {            
+  std::vector< Node > lemmas; 
+  // register constraints
+  Trace("nl-ext-debug") << "Register bound constraints..." << std::endl;
+  for (context::CDList<Assertion>::const_iterator it =
+           d_containing.facts_begin();
+       it != d_containing.facts_end(); ++it) {
+    Node lit = (*it).assertion;
+    bool polarity = lit.getKind() != kind::NOT;
+    Node atom = lit.getKind() == kind::NOT ? lit[0] : lit;
+    registerConstraint(atom);
+    bool is_false_lit = false_asserts.find(lit) != false_asserts.end();
+    // add information about bounds to variables
+    std::map<Node, std::map<Node, ConstraintInfo> >::iterator itc =
+        d_c_info.find(atom);
+    std::map<Node, std::map<Node, bool> >::iterator itcm =
+        d_c_info_maxm.find(atom);
+    if (itc != d_c_info.end()) {
+      Assert(itcm != d_c_info_maxm.end());
+      for (std::map<Node, ConstraintInfo>::iterator itcc = itc->second.begin();
+           itcc != itc->second.end(); ++itcc) {
+        Node x = itcc->first;
+        Node coeff = itcc->second.d_coeff;
+        Node rhs = itcc->second.d_rhs;
+        Kind type = itcc->second.d_type;
+        Node exp = lit;
+        if (!polarity) {
+          // reverse
+          if (type == kind::EQUAL) {
+            // we will take the strict inequality in the direction of the
+            // model
+            Node lhs = QuantArith::mkCoeffTerm(coeff, x);
+            Node query = NodeManager::currentNM()->mkNode(kind::GT, lhs, rhs);
+            Node query_mv = computeModelValue(query, 1);
+            if (query_mv == d_true) {
+              exp = query;
+              type = kind::GT;
+            } else {
+              Assert(query_mv == d_false);
+              exp = NodeManager::currentNM()->mkNode(kind::LT, lhs, rhs);
+              type = kind::LT;
+            }
+          } else {
+            type = negateKind(type);
+          }
+        }
+        // add to status if maximal degree
+        d_ci_max[x][coeff][rhs] = itcm->second.find(x) != itcm->second.end();
+        if (Trace.isOn("nl-ext-bound-debug2")) {
+          Node t = QuantArith::mkCoeffTerm(coeff, x);
+          Trace("nl-ext-bound-debug2")
+              << "Add Bound: " << t << " " << type << " " << rhs << " by "
+              << exp << std::endl;
+        }
+        bool updated = true;
+        std::map<Node, Kind>::iterator its = d_ci[x][coeff].find(rhs);
+        if (its == d_ci[x][coeff].end()) {
+          d_ci[x][coeff][rhs] = type;
+          d_ci_exp[x][coeff][rhs] = exp;
+        } else if (type != its->second) {
+          Trace("nl-ext-bound-debug2")
+              << "Joining kinds : " << type << " " << its->second << std::endl;
+          Kind jk = joinKinds(type, its->second);
+          if (jk == kind::UNDEFINED_KIND) {
+            updated = false;
+          } else if (jk != its->second) {
+            if (jk == type) {
+              d_ci[x][coeff][rhs] = type;
+              d_ci_exp[x][coeff][rhs] = exp;
+            } else {
+              d_ci[x][coeff][rhs] = jk;
+              d_ci_exp[x][coeff][rhs] = NodeManager::currentNM()->mkNode(
+                  kind::AND, d_ci_exp[x][coeff][rhs], exp);
+            }
+          } else {
+            updated = false;
+          }
+        }
+        if (Trace.isOn("nl-ext-bound")) {
+          if (updated) {
+            Trace("nl-ext-bound") << "Bound: ";
+            debugPrintBound("nl-ext-bound", coeff, x, d_ci[x][coeff][rhs], rhs);
+            Trace("nl-ext-bound") << " by " << d_ci_exp[x][coeff][rhs];
+            if (d_ci_max[x][coeff][rhs]) {
+              Trace("nl-ext-bound") << ", is max degree";
+            }
+            Trace("nl-ext-bound") << std::endl;
+          }
+        }
+        // compute if bound is not satisfied, and store what is required
+        // for a possible refinement
+        if (options::nlExtTangentPlanes()) {
+          if (is_false_lit) {
+            Node rhs_v = computeModelValue(rhs, 0);
+            Node x_v = computeModelValue(x, 0);
+            if( rhs_v.isConst() && x_v.isConst() ){
+              bool needsRefine = false;
+              bool refineDir;
+              if (rhs_v == x_v) {
+                if (type == kind::GT) {
+                  needsRefine = true;
+                  refineDir = true;
+                } else if (type == kind::LT) {
+                  needsRefine = true;
+                  refineDir = false;
+                }
+              } else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) {
+                if (type != kind::GT && type != kind::GEQ) {
+                  needsRefine = true;
+                  refineDir = false;
+                }
+              } else {
+                if (type != kind::LT && type != kind::LEQ) {
+                  needsRefine = true;
+                  refineDir = true;
+                }
+              }
+              Trace("nl-ext-tplanes-cons-debug")
+                  << "...compute if bound corresponds to a required "
+                     "refinement"
+                  << std::endl;
+              Trace("nl-ext-tplanes-cons-debug")
+                  << "...M[" << x << "] = " << x_v << ", M[" << rhs
+                  << "] = " << rhs_v << std::endl;
+              Trace("nl-ext-tplanes-cons-debug") << "...refine = " << needsRefine
+                                                 << "/" << refineDir << std::endl;
+              if (needsRefine) {
+                Trace("nl-ext-tplanes-cons")
+                    << "---> By " << lit << " and since M[" << x << "] = " << x_v
+                    << ", M[" << rhs << "] = " << rhs_v << ", ";
+                Trace("nl-ext-tplanes-cons")
+                    << "monomial " << x << " should be "
+                    << (refineDir ? "larger" : "smaller") << std::endl;
+                d_tplane_refine_dir[x][refineDir] = true;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  // reflexive constraints
+  Node null_coeff;
+  for (unsigned j = 0; j < d_mterms.size(); j++) {
+    Node n = d_mterms[j];
+    d_ci[n][null_coeff][n] = kind::EQUAL;
+    d_ci_exp[n][null_coeff][n] = d_true;
+    d_ci_max[n][null_coeff][n] = false;
+  }
+
+  Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl;
+  
+  for (unsigned k = 0; k < d_mterms.size(); k++) {
+    Node x = d_mterms[k];
+    Trace("nl-ext-bound-debug")
+        << "Process bounds for " << x << " : " << std::endl;
+    std::map<Node, std::vector<Node> >::iterator itm =
+        d_m_contain_parent.find(x);
+    if (itm != d_m_contain_parent.end()) {
+      Trace("nl-ext-bound-debug") << "...has " << itm->second.size()
+                                  << " parent monomials." << std::endl;
+      // check derived bounds
+      std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc =
+          d_ci.find(x);
+      if (itc != d_ci.end()) {
+        for (std::map<Node, std::map<Node, Kind> >::iterator itcc =
+                 itc->second.begin();
+             itcc != itc->second.end(); ++itcc) {
+          Node coeff = itcc->first;
+          Node t = QuantArith::mkCoeffTerm(coeff, x);
+          for (std::map<Node, Kind>::iterator itcr = itcc->second.begin();
+               itcr != itcc->second.end(); ++itcr) {
+            Node rhs = itcr->first;
+            // only consider this bound if maximal degree
+            if (d_ci_max[x][coeff][rhs]) {
+              Kind type = itcr->second;
+              for (unsigned j = 0; j < itm->second.size(); j++) {
+                Node y = itm->second[j];
+                Assert(d_m_contain_mult[x].find(y) !=
+                       d_m_contain_mult[x].end());
+                Node mult = d_m_contain_mult[x][y];
+                // x <k> t => m*x <k'> t  where y = m*x
+                // get the sign of mult
+                Node mmv = computeModelValue(mult);
+                Trace("nl-ext-bound-debug2")
+                    << "Model value of " << mult << " is " << mmv << std::endl;
+                if(mmv.isConst()){
+                  int mmv_sign = mmv.getConst<Rational>().sgn();
+                  Trace("nl-ext-bound-debug2")
+                      << "  sign of " << mmv << " is " << mmv_sign << std::endl;
+                  if (mmv_sign != 0) {
+                    Trace("nl-ext-bound-debug")
+                        << "  from " << x << " * " << mult << " = " << y
+                        << " and " << t << " " << type << " " << rhs
+                        << ", infer : " << std::endl;
+                    Kind infer_type =
+                        mmv_sign == -1 ? reverseRelationKind(type) : type;
+                    Node infer_lhs =
+                        NodeManager::currentNM()->mkNode(kind::MULT, mult, t);
+                    Node infer_rhs =
+                        NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs);
+                    Node infer = NodeManager::currentNM()->mkNode(
+                        infer_type, infer_lhs, infer_rhs);
+                    Trace("nl-ext-bound-debug") << "     " << infer << std::endl;
+                    infer = Rewriter::rewrite(infer);
+                    Trace("nl-ext-bound-debug2")
+                        << "     ...rewritten : " << infer << std::endl;
+                    // check whether it is false in model for abstraction
+                    Node infer_mv = computeModelValue(infer, 1);
+                    Trace("nl-ext-bound-debug")
+                        << "       ...infer model value is " << infer_mv
+                        << std::endl;
+                    if (infer_mv == d_false) {
+                      Node exp = NodeManager::currentNM()->mkNode(
+                          kind::AND,
+                          NodeManager::currentNM()->mkNode(
+                              mmv_sign == 1 ? kind::GT : kind::LT, mult, d_zero),
+                          d_ci_exp[x][coeff][rhs]);
+                      Node iblem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
+                                                                    exp, infer);
+                      Node pr_iblem = iblem;
+                      iblem = Rewriter::rewrite(iblem);
+                      bool introNewTerms = hasNewMonomials(iblem, d_ms);
+                      Trace("nl-ext-bound-lemma")
+                          << "*** Bound inference lemma : " << iblem
+                          << " (pre-rewrite : " << pr_iblem << ")" << std::endl;
+                      // Trace("nl-ext-bound-lemma") << "       intro new
+                      // monomials = " << introNewTerms << std::endl;
+                      if (!introNewTerms) {
+                        lemmas.push_back(iblem);
+                      } else {
+                        nt_lemmas.push_back(iblem);
+                      }
+                    }
+                  } else {
+                    Trace("nl-ext-bound-debug") << "     ...coefficient " << mult
+                                                << " is zero." << std::endl;
+                  }
+                }else{
+                  Trace("nl-ext-bound-debug") << "     ...coefficient " << mult
+                                              << " is non-constant (probably transcendental)." << std::endl;
+                }
+              }
+            }
+          }
+        }
+      }
+    } else {
+      Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl;
+    }
+  }
+  return lemmas;
+}
+
+std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& false_asserts ) {
+  std::vector< Node > lemmas; 
+  Trace("nl-ext") << "Get factoring lemmas..." << std::endl;
+  for (context::CDList<Assertion>::const_iterator it =
+           d_containing.facts_begin();
+       it != d_containing.facts_end(); ++it) {
+    Node lit = (*it).assertion;
+    bool polarity = lit.getKind() != kind::NOT;
+    Node atom = lit.getKind() == kind::NOT ? lit[0] : lit;
+    if( false_asserts.find(lit) != false_asserts.end() || d_skolem_atoms.find(atom)!=d_skolem_atoms.end() ){
+      std::map<Node, Node> msum;
+      if (QuantArith::getMonomialSumLit(atom, msum)) {
+        Trace("nl-ext-factor") << "Factoring for literal " << lit << ", monomial sum is : " << std::endl;
+        if (Trace.isOn("nl-ext-factor")) {
+          QuantArith::debugPrintMonomialSum(msum, "nl-ext-factor");
+        }
+        std::map< Node, std::vector< Node > > factor_to_mono;
+        std::map< Node, std::vector< Node > > factor_to_mono_orig;
+        for( std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
+          if( !itm->first.isNull() ){
+            if( itm->first.getKind()==NONLINEAR_MULT ){
+              std::vector< Node > children;
+              for( unsigned i=0; i<itm->first.getNumChildren(); i++ ){
+                children.push_back( itm->first[i] );
+              }
+              std::map< Node, bool > processed;
+              for( unsigned i=0; i<itm->first.getNumChildren(); i++ ){
+                if( processed.find( itm->first[i] )==processed.end() ){
+                  processed[itm->first[i]] = true;
+                  children[i] = d_one;
+                  if( !itm->second.isNull() ){
+                    children.push_back( itm->second );
+                  }
+                  Node val = NodeManager::currentNM()->mkNode( kind::MULT, children );
+                  if( !itm->second.isNull() ){
+                    children.pop_back();
+                  }
+                  children[i] = itm->first[i];
+                  val = Rewriter::rewrite( val );
+                  factor_to_mono[itm->first[i]].push_back( val );
+                  factor_to_mono_orig[itm->first[i]].push_back( itm->first );
+                }
+              }
+            } /* else{
+              factor_to_mono[itm->first].push_back( itm->second.isNull() ? d_one : itm->second );
+              factor_to_mono_orig[itm->first].push_back( itm->first );
+            }*/
+          }
+        }
+        for( std::map< Node, std::vector< Node > >::iterator itf = factor_to_mono.begin(); itf != factor_to_mono.end(); ++itf ){
+          if( itf->second.size()>1 ){
+            Node sum = NodeManager::currentNM()->mkNode( kind::PLUS, itf->second );
+            sum = Rewriter::rewrite( sum );
+            Trace("nl-ext-factor") << "* Factored sum for " << itf->first << " : " << sum << std::endl;
+            Node kf = getFactorSkolem( sum, lemmas ); 
+            std::vector< Node > poly;
+            poly.push_back( NodeManager::currentNM()->mkNode( kind::MULT, itf->first, kf ) );
+            std::map< Node, std::vector< Node > >::iterator itfo = factor_to_mono_orig.find( itf->first );
+            Assert( itfo!=factor_to_mono_orig.end() );
+            for( std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
+              if( std::find( itfo->second.begin(), itfo->second.end(), itm->first )==itfo->second.end() ){
+                poly.push_back( QuantArith::mkCoeffTerm(itm->second, itm->first.isNull() ? d_one : itm->first) );
+              }
+            }
+            Node polyn = poly.size()==1 ? poly[0] : NodeManager::currentNM()->mkNode( kind::PLUS, poly );
+            Trace("nl-ext-factor") << "...factored polynomial : " << polyn << std::endl;
+            Node conc_lit = NodeManager::currentNM()->mkNode( atom.getKind(), polyn, d_zero );
+            conc_lit = Rewriter::rewrite( conc_lit );
+            d_skolem_atoms.insert( conc_lit );
+            if( !polarity ){
+              conc_lit = conc_lit.negate();
+            }
+            
+            std::vector< Node > lemma_disj;
+            lemma_disj.push_back( lit.negate() );
+            lemma_disj.push_back( conc_lit );
+            Node flem = NodeManager::currentNM()->mkNode( kind::OR, lemma_disj );
+            Trace("nl-ext-factor") << "...lemma is " << flem << std::endl;
+            lemmas.push_back( flem ); 
+          }
+        }
+      }
+    }
+  }
+  return lemmas;
+}
+
+Node NonlinearExtension::getFactorSkolem( Node n, std::vector< Node >& lemmas ) {
+  std::map< Node, Node >::iterator itf = d_factor_skolem.find( n );
+  if( itf==d_factor_skolem.end() ){
+    Node k = NodeManager::currentNM()->mkSkolem( "kf", n.getType() );
+    Node k_eq = Rewriter::rewrite( k.eqNode( n ) );
+    d_skolem_atoms.insert( k_eq );
+    lemmas.push_back( k_eq );
+    d_factor_skolem[n] = k;
+    return k;
+  }else{
+    return itf->second;
+  }  
+}
+                    
+std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() {            
+  std::vector< Node > lemmas; 
+  Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..." << std::endl;
+  for (unsigned j = 0; j < d_mterms.size(); j++) {
+    Node a = d_mterms[j];
+    std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca =
+        d_ci.find(a);
+    if (itca != d_ci.end()) {
+      for (unsigned k = (j + 1); k < d_mterms.size(); k++) {
+        Node b = d_mterms[k];
+        std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator
+            itcb = d_ci.find(b);
+        if (itcb != d_ci.end()) {
+          Trace("nl-ext-rbound-debug") << "resolution inferences : compare "
+                                       << a << " and " << b << std::endl;
+          // if they have common factors
+          std::map<Node, Node>::iterator ita = d_mono_diff[a].find(b);
+          if (ita != d_mono_diff[a].end()) {
+            std::map<Node, Node>::iterator itb = d_mono_diff[b].find(a);
+            Assert(itb != d_mono_diff[b].end());
+            Node mv_a = computeModelValue(ita->second, 1);
+            Assert(mv_a.isConst());
+            int mv_a_sgn = mv_a.getConst<Rational>().sgn();
+            Assert(mv_a_sgn != 0);
+            Node mv_b = computeModelValue(itb->second, 1);
+            Assert(mv_b.isConst());
+            int mv_b_sgn = mv_b.getConst<Rational>().sgn();
+            Assert(mv_b_sgn != 0);
+            Trace("nl-ext-rbound") << "Get resolution inferences for [a] "
+                                   << a << " vs [b] " << b << std::endl;
+            Trace("nl-ext-rbound")
+                << "  [a] factor is " << ita->second
+                << ", sign in model = " << mv_a_sgn << std::endl;
+            Trace("nl-ext-rbound")
+                << "  [b] factor is " << itb->second
+                << ", sign in model = " << mv_b_sgn << std::endl;
+
+            std::vector<Node> exp;
+            // bounds of a
+            for (std::map<Node, std::map<Node, Kind> >::iterator itcac =
+                     itca->second.begin();
+                 itcac != itca->second.end(); ++itcac) {
+              Node coeff_a = itcac->first;
+              for (std::map<Node, Kind>::iterator itcar =
+                       itcac->second.begin();
+                   itcar != itcac->second.end(); ++itcar) {
+                Node rhs_a = itcar->first;
+                Node rhs_a_res_base = NodeManager::currentNM()->mkNode(
+                    kind::MULT, itb->second, rhs_a);
+                rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
+                if (!hasNewMonomials(rhs_a_res_base, d_ms)) {
+                  Kind type_a = itcar->second;
+                  exp.push_back(d_ci_exp[a][coeff_a][rhs_a]);
+
+                  // bounds of b
+                  for (std::map<Node, std::map<Node, Kind> >::iterator itcbc =
+                           itcb->second.begin();
+                       itcbc != itcb->second.end(); ++itcbc) {
+                    Node coeff_b = itcbc->first;
+                    Node rhs_a_res =
+                        QuantArith::mkCoeffTerm(coeff_b, rhs_a_res_base);
+                    for (std::map<Node, Kind>::iterator itcbr =
+                             itcbc->second.begin();
+                         itcbr != itcbc->second.end(); ++itcbr) {
+                      Node rhs_b = itcbr->first;
+                      Node rhs_b_res = NodeManager::currentNM()->mkNode(
+                          kind::MULT, ita->second, rhs_b);
+                      rhs_b_res = QuantArith::mkCoeffTerm(coeff_a, rhs_b_res);
+                      rhs_b_res = Rewriter::rewrite(rhs_b_res);
+                      if (!hasNewMonomials(rhs_b_res, d_ms)) {
+                        Kind type_b = itcbr->second;
+                        exp.push_back(d_ci_exp[b][coeff_b][rhs_b]);
+                        if (Trace.isOn("nl-ext-rbound")) {
+                          Trace("nl-ext-rbound") << "* try bounds : ";
+                          debugPrintBound("nl-ext-rbound", coeff_a, a, type_a,
+                                          rhs_a);
+                          Trace("nl-ext-rbound") << std::endl;
+                          Trace("nl-ext-rbound") << "               ";
+                          debugPrintBound("nl-ext-rbound", coeff_b, b, type_b,
+                                          rhs_b);
+                          Trace("nl-ext-rbound") << std::endl;
+                        }
+                        Kind types[2];
+                        for (unsigned r = 0; r < 2; r++) {
+                          Node pivot_factor =
+                              r == 0 ? itb->second : ita->second;
+                          int pivot_factor_sign =
+                              r == 0 ? mv_b_sgn : mv_a_sgn;
+                          types[r] = r == 0 ? type_a : type_b;
+                          if (pivot_factor_sign == (r == 0 ? 1 : -1)) {
+                            types[r] = reverseRelationKind(types[r]);
+                          }
+                          if (pivot_factor_sign == 1) {
+                            exp.push_back(NodeManager::currentNM()->mkNode(
+                                kind::GT, pivot_factor, d_zero));
+                          } else {
+                            exp.push_back(NodeManager::currentNM()->mkNode(
+                                kind::LT, pivot_factor, d_zero));
+                          }
+                        }
+                        Kind jk = transKinds(types[0], types[1]);
+                        Trace("nl-ext-rbound-debug")
+                            << "trans kind : " << types[0] << " + "
+                            << types[1] << " = " << jk << std::endl;
+                        if (jk != kind::UNDEFINED_KIND) {
+                          Node conc = NodeManager::currentNM()->mkNode(
+                              jk, rhs_a_res, rhs_b_res);
+                          Node conc_mv = computeModelValue(conc, 1);
+                          if (conc_mv == d_false) {
+                            Node rblem = NodeManager::currentNM()->mkNode(
+                                kind::IMPLIES,
+                                NodeManager::currentNM()->mkNode(kind::AND,
+                                                                 exp),
+                                conc);
+                            Trace("nl-ext-rbound-lemma-debug")
+                                << "Resolution bound lemma "
+                                   "(pre-rewrite) "
+                                   ": "
+                                << rblem << std::endl;
+                            rblem = Rewriter::rewrite(rblem);
+                            Trace("nl-ext-rbound-lemma")
+                                << "Resolution bound lemma : " << rblem
+                                << std::endl;
+                            lemmas.push_back(rblem);
+                          }
+                        }
+                        exp.pop_back();
+                        exp.pop_back();
+                        exp.pop_back();
+                      }
+                    }
+                  }
+                  exp.pop_back();
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  return lemmas;
+}
+                    
+std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
+  std::vector< Node > lemmas;
+  Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl;
+  for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
+    std::map< Node, Node > mv_to_term;
+    for( std::map< Node, Node >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
+      Node t = itt->second;
+      Assert( d_mv[1].find( t )!=d_mv[1].end() );
+      Node tv = d_mv[1][t];
+      mv_to_term[tv] = t;
+      // easy model-based bounds  (TODO: make these unconditional?)
+      if( it->first==kind::SINE ){
+        Assert( tv.isConst() );
+        /*
+        if( tv.getConst<Rational>() > d_one.getConst<Rational>() ){
+          lemmas.push_back( NodeManager::currentNM()->mkNode( kind::LEQ, t, d_one ) );
+        }else if( tv.getConst<Rational>() < d_neg_one.getConst<Rational>() ){
+          lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, t, d_neg_one ) );
+        }
+        */
+        /*
+        if( tv.getConst<Rational>().sgn()!=0 ){
+          //symmetry (model-based)
+          Node neg_tv = NodeManager::currentNM()->mkConst( -tv.getConst<Rational>() );
+          if( mv_to_term.find( neg_tv )!=mv_to_term.end() ){
+            Node sum = NodeManager::currentNM()->mkNode( kind::PLUS, mv_to_term[neg_tv][0], t[0] ); 
+            Node res = computeModelValue( sum, 0 );
+            if( !res.isConst() || res.getConst<Rational>().sgn()!=0 ){
+              Node tsum = NodeManager::currentNM()->mkNode( kind::PLUS, mv_to_term[neg_tv], t ); 
+              Node sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, tsum.eqNode( d_zero ), sum.eqNode( d_zero ) );
+              lemmas.push_back( sym_lem );
+            }
+          }
+        }
+        */
+      }else if( it->first==kind::EXPONENTIAL ){
+        if( tv.getConst<Rational>().sgn()==-1 ){
+          lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GT, t, d_zero ) );
+        }
+      }
+      //initial refinements
+      if( d_tf_initial_refine.find( t )==d_tf_initial_refine.end() ){
+        d_tf_initial_refine[t] = true;
+        Node lem;
+        if( it->first==kind::SINE ){
+          Node symn = NodeManager::currentNM()->mkNode( kind::SINE, 
+                        NodeManager::currentNM()->mkNode( kind::MULT, d_neg_one, t[0] ) );
+          symn = Rewriter::rewrite( symn );
+          //can assume its basis since phase is split over 0
+          d_trig_is_base[symn] = true;
+          Assert( d_trig_is_base.find( t ) != d_trig_is_base.end() );
+          std::vector< Node > children;
+          
+          lem = NodeManager::currentNM()->mkNode( kind::AND, 
+                  //bounds
+                  NodeManager::currentNM()->mkNode( kind::AND,
+                    NodeManager::currentNM()->mkNode( kind::LEQ, t, d_one ),
+                    NodeManager::currentNM()->mkNode( kind::GEQ, t, d_neg_one ) ),
+                  //symmetry
+                  NodeManager::currentNM()->mkNode( kind::PLUS, t, symn ).eqNode( d_zero ),
+                  //sign
+                  NodeManager::currentNM()->mkNode( kind::EQUAL, 
+                    NodeManager::currentNM()->mkNode( kind::LT, t[0], d_zero ),
+                    NodeManager::currentNM()->mkNode( kind::LT, t, d_zero ) ),
+                  //zero val
+                  NodeManager::currentNM()->mkNode( kind::EQUAL, 
+                    NodeManager::currentNM()->mkNode( kind::GT, t[0], d_zero ),
+                    NodeManager::currentNM()->mkNode( kind::GT, t, d_zero ) ) );
+           lem = NodeManager::currentNM()->mkNode( kind::AND, lem,
+                  //zero tangent
+                  NodeManager::currentNM()->mkNode( kind::AND,
+                    NodeManager::currentNM()->mkNode( kind::IMPLIES,
+                      NodeManager::currentNM()->mkNode( kind::GT, t[0], d_zero ),
+                      NodeManager::currentNM()->mkNode( kind::LT, t, t[0] ) ),
+                    NodeManager::currentNM()->mkNode( kind::IMPLIES,
+                      NodeManager::currentNM()->mkNode( kind::LT, t[0], d_zero ),
+                      NodeManager::currentNM()->mkNode( kind::GT, t, t[0] ) ) ),
+                  //pi tangent
+                  NodeManager::currentNM()->mkNode( kind::AND,
+                    NodeManager::currentNM()->mkNode( kind::IMPLIES,
+                      NodeManager::currentNM()->mkNode( kind::LT, t[0], d_pi ),
+                      NodeManager::currentNM()->mkNode( kind::LT, t, NodeManager::currentNM()->mkNode( kind::MINUS, d_pi, t[0] ) ) ),
+                    NodeManager::currentNM()->mkNode( kind::IMPLIES,
+                      NodeManager::currentNM()->mkNode( kind::GT, t[0], d_pi_neg ),
+                      NodeManager::currentNM()->mkNode( kind::GT, t, NodeManager::currentNM()->mkNode( kind::MINUS, d_pi_neg, t[0] ) ) ) ) );
+        }else if( it->first==kind::EXPONENTIAL ){
+          // exp(x)>0 ^ x < 0 <=> exp( x ) < 1 ^ ( x = 0 V exp( x ) > x + 1 ) 
+          lem = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::EQUAL, t[0].eqNode(d_zero), t.eqNode(d_one)),
+                  NodeManager::currentNM()->mkNode( kind::EQUAL, 
+                    NodeManager::currentNM()->mkNode( kind::LT, t[0], d_zero ),
+                    NodeManager::currentNM()->mkNode( kind::LT, t, d_one ) ),
+                  NodeManager::currentNM()->mkNode( kind::OR, 
+                    NodeManager::currentNM()->mkNode( kind::LEQ, t[0], d_zero ),
+                    NodeManager::currentNM()->mkNode( kind::GT, t, NodeManager::currentNM()->mkNode( kind::PLUS, t[0], d_one ) ) ) );
+                    
+        }
+        if( !lem.isNull() ){
+          lemmas.push_back( lem );
+        }
+      }
+    }
+  }
+  
+  return lemmas;
+}
+
+std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
+  std::vector< Node > lemmas;
+  Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..." << std::endl;
+  
+  //sort arguments of all transcendentals
+  std::map< Kind, std::vector< Node > > sorted_tf_args;
+  std::map< Kind, std::map< Node, Node > > tf_arg_to_term;
+  
+  for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
+    for( std::map< Node, Node >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
+      computeModelValue( itt->second[0], 1 );
+      Assert( d_mv[1].find( itt->second[0] )!=d_mv[1].end() );
+      if( d_mv[1][itt->second[0]].isConst() ){
+        Trace("nl-ext-tf-mono-debug") << "...tf term : " << itt->second[0] << std::endl;
+        sorted_tf_args[ it->first ].push_back( itt->second[0] );
+        tf_arg_to_term[ it->first ][ itt->second[0] ] = itt->second;
+      }
+    } 
+  }
+  
+  SortNonlinearExtension smv;
+  smv.d_nla = this;
+  //sort by concrete values
+  smv.d_order_type = 0;
+  smv.d_reverse_order = true;
+  for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
+    Kind k = it->first;
+    if( !sorted_tf_args[k].empty() ){
+      std::sort( sorted_tf_args[k].begin(), sorted_tf_args[k].end(), smv );
+      Trace("nl-ext-tf-mono") << "Sorted transcendental function list for " << k << " : " << std::endl;
+      for( unsigned i=0; i<sorted_tf_args[it->first].size(); i++ ){
+        Node targ = sorted_tf_args[k][i];
+        Assert( d_mv[1].find( targ )!=d_mv[1].end() );
+        Trace("nl-ext-tf-mono") << "  " << targ << " -> " << d_mv[1][targ] << std::endl;
+        Node t = tf_arg_to_term[k][targ];
+        Assert( d_mv[1].find( t )!=d_mv[1].end() );
+        Trace("nl-ext-tf-mono") << "     f-val : " << d_mv[1][t] << std::endl;
+      }
+      std::vector< int > mdirs;
+      std::vector< Node > mpoints;
+      std::vector< Node > mpoints_vals;
+      if( it->first==kind::SINE ){
+        mdirs.push_back( -1 );
+        mpoints.push_back( d_pi );
+        mdirs.push_back( 1 );
+        mpoints.push_back( d_pi_2 );
+        mdirs.push_back( -1 );
+        mpoints.push_back( d_pi_neg_2 );
+        mdirs.push_back( 0 );
+        mpoints.push_back( d_pi_neg );
+      }else if( it->first==kind::EXPONENTIAL ){
+        mdirs.push_back( 1 );
+        mpoints.push_back( Node::null() );
+      }
+      if( !mpoints.empty() ){
+        //get model values for points
+        for( unsigned i=0; i<mpoints.size(); i++ ){
+          Node mpv;
+          if( !mpoints[i].isNull() ){
+            mpv = computeModelValue( mpoints[i], 1 );
+            Assert( mpv.isConst() );
+          }
+          mpoints_vals.push_back( mpv );
+        }
+        
+        unsigned mdir_index = 0;
+        int monotonic_dir = -1;
+        Node mono_bounds[2];
+        Node targ, targval, t, tval;
+        for( unsigned i=0; i<sorted_tf_args[it->first].size(); i++ ){
+          Node sarg = sorted_tf_args[k][i];
+          Assert( d_mv[1].find( sarg )!=d_mv[1].end() );
+          Node sargval = d_mv[1][sarg];
+          Assert( sargval.isConst() ); 
+          Node s = tf_arg_to_term[k][ sarg ];
+          Assert( d_mv[1].find( s )!=d_mv[1].end() );
+          Node sval = d_mv[1][s];
+          Assert( sval.isConst() ); 
+        
+          //increment to the proper monotonicity region
+          bool increment = true;
+          while( increment && mdir_index<mdirs.size() ){
+            increment = false;
+            if( mpoints[mdir_index].isNull() ){
+              increment = true;
+            }else{
+              Node pval = mpoints_vals[mdir_index];
+              Assert( pval.isConst() );
+              if( sargval.getConst<Rational>() < pval.getConst<Rational>() ){
+                increment = true;
+                Trace("nl-ext-tf-mono") << "...increment at " << sarg << " since model value is less than " << mpoints[mdir_index] << std::endl;
+              }
+            }
+            if( increment ){
+              tval = Node::null();
+              monotonic_dir = mdirs[mdir_index];
+              mono_bounds[1] = mpoints[mdir_index];
+              mdir_index++;
+              if( mdir_index<mdirs.size() ){
+                mono_bounds[0] = mpoints[mdir_index];
+              }else{
+                mono_bounds[0] = Node::null();
+              }
+            }
+          }
+        
+           
+          if( !tval.isNull() ){
+            Node mono_lem;
+            if( monotonic_dir==1 && sval.getConst<Rational>() > tval.getConst<Rational>() ){
+              mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, 
+                            NodeManager::currentNM()->mkNode( kind::GEQ, targ, sarg ),
+                            NodeManager::currentNM()->mkNode( kind::GEQ, t, s ) );
+            }else if( monotonic_dir==-1 && sval.getConst<Rational>() < tval.getConst<Rational>() ){
+              mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, 
+                            NodeManager::currentNM()->mkNode( kind::LEQ, targ, sarg ),
+                            NodeManager::currentNM()->mkNode( kind::LEQ, t, s ) );
+            }
+            if( !mono_lem.isNull() ){        
+              if( !mono_bounds[0].isNull() ){
+                Assert( !mono_bounds[1].isNull() );
+                mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, 
+                             NodeManager::currentNM()->mkNode( kind::AND, 
+                               mkBounded( mono_bounds[0], targ, mono_bounds[1] ), 
+                               mkBounded( mono_bounds[0], sarg, mono_bounds[1] ) ),
+                             mono_lem );
+              }      
+              Trace("nl-ext-tf-mono") << "Monotonicity lemma : " << mono_lem << std::endl;
+              lemmas.push_back( mono_lem );
+            }
+          }
+          targ = sarg;
+          targval = sargval;
+          t = s;
+          tval = sval;
+        }
+      }
+    }
+  }
+  
+  
+  
+  
+  return lemmas;
+}
+  
+  
+Node NonlinearExtension::getTaylor( Node tf, Node x, unsigned n, std::vector< Node >& lemmas ) {
+  Node i_exp_base_term = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MINUS, x, tf[0] ) );
+  Node i_exp_base = getFactorSkolem( i_exp_base_term, lemmas );
+  Node i_derv = tf;
+  Node i_fact = d_one;
+  Node i_exp = d_one;
+  int i_derv_status = 0;
+  unsigned counter = 0;
+  std::vector< Node > sum;
+  do {
+    counter++;
+    if( tf.getKind()==kind::EXPONENTIAL ){
+      //unchanged
+    }else if( tf.getKind()==kind::SINE ){
+      if( i_derv_status%2==1 ){
+        Node arg = NodeManager::currentNM()->mkNode( kind::MINUS, 
+                     NodeManager::currentNM()->mkNode( kind::MULT, 
+                       NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ),
+                       NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI ) ),
+                     tf[0] );
+        i_derv = NodeManager::currentNM()->mkNode( kind::SINE, arg );
+      }else{
+        i_derv = tf;
+      }
+      if( i_derv_status>=2 ){
+        i_derv = NodeManager::currentNM()->mkNode( kind::MINUS, d_zero, i_derv );
+      }
+      i_derv = Rewriter::rewrite( i_derv );
+      i_derv_status = i_derv_status==3 ? 0 : i_derv_status+1;
+    }
+    Node curr = NodeManager::currentNM()->mkNode( kind::MULT, 
+                  NodeManager::currentNM()->mkNode( kind::DIVISION, i_derv, i_fact ), i_exp );
+    sum.push_back( curr );
+    i_fact = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, NodeManager::currentNM()->mkConst( Rational( counter ) ) ) );
+    i_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, i_exp_base, i_exp ) );
+  }while( counter<n );
+  return sum.size()==1 ? sum[0] : NodeManager::currentNM()->mkNode( kind::PLUS, sum );
+}
+                    
 }  // namespace arith
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index dc93046c0..1a19eb67a 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -86,17 +86,17 @@ class NonlinearExtension {
   // Check assertions for consistency in the effort LAST_CALL with a subset of
   // the assertions, false_asserts, evaluate to false in the current model.
   void checkLastCall(const std::vector<Node>& assertions,
-                     const std::set<Node>& false_asserts);
-
-  // Returns a vector containing a split on whether each term is 0 or not for
-  // those terms that have not been split on in the current context.
-  std::vector<Node> splitOnZeros(const std::vector<Node>& terms);
+                     const std::set<Node>& false_asserts,
+                     const std::vector<Node>& xts);
 
   static bool isArithKind(Kind k);
   static Node mkLit(Node a, Node b, int status, int orderType = 0);
   static Node mkAbs(Node a);
+  static Node mkValidPhase(Node a, Node pi);
+  static Node mkBounded( Node l, Node a, Node u );
   static Kind joinKinds(Kind k1, Kind k2);
   static Kind transKinds(Kind k1, Kind k2);
+  static bool isTranscendentalKind(Kind k);
   Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const;
 
   // register monomial
@@ -171,6 +171,9 @@ class NonlinearExtension {
   // cache of all lemmas sent
   NodeSet d_lemmas;
   NodeSet d_zero_split;
+  
+  // literals with Skolems (need not be satisfied by model)
+  NodeSet d_skolem_atoms;
 
   // utilities
   Node d_zero;
@@ -197,8 +200,71 @@ class NonlinearExtension {
   std::map<Node, Node> d_mv[2];
 
   // ordering, stores variables and 0,1,-1
-  std::map<unsigned, NodeMultiset> d_order_vars;
+  std::map<Node, unsigned> d_order_vars;
   std::vector<Node> d_order_points;
+  
+  //transcendent functions
+  std::map<Node, Node> d_trig_base;
+  std::map<Node, bool> d_trig_is_base;
+  std::map< Node, bool > d_tf_initial_refine;
+  Node d_pi;
+  Node d_pi_2;
+  Node d_pi_neg_2;
+  Node d_pi_neg;
+  Node d_pi_bound[2];
+  
+  void mkPi();
+  void getCurrentPiBounds( std::vector< Node >& lemmas );
+private:
+  //per last-call effort check
+  
+  //information about monomials
+  std::vector< Node > d_ms;
+  std::vector< Node > d_ms_vars;
+  std::map<Node, bool> d_ms_proc;
+  std::vector<Node> d_mterms;  
+  //list of monomials with factors whose model value is non-constant in model 
+  //  e.g. y*cos( x )
+  std::map<Node, bool> d_m_nconst_factor;
+  // If ( m, p1, true ), then it would help satisfiability if m were ( >
+  // if p1=true, < if p1=false )
+  std::map<Node, std::map<bool, bool> > d_tplane_refine_dir;
+  // term -> coeff -> rhs -> ( status, exp, b ),
+  //   where we have that : exp =>  ( coeff * term <status> rhs )
+  //   b is true if degree( term ) >= degree( rhs )
+  std::map<Node, std::map<Node, std::map<Node, Kind> > > d_ci;
+  std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp;
+  std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max;
+  
+  //information about transcendental functions
+  std::map< Kind, std::map< Node, Node > > d_tf_rep_map;  
+  
+  // factor skolems
+  std::map< Node, Node > d_factor_skolem;
+  Node getFactorSkolem( Node n, std::vector< Node >& lemmas );
+  
+  Node getTaylor( Node tf, Node x, unsigned n, std::vector< Node >& lemmas );
+private:
+  // Returns a vector containing a split on whether each term is 0 or not for
+  // those terms that have not been split on in the current context.
+  std::vector<Node> checkSplitZero();
+  
+  std::vector<Node> checkMonomialSign();
+  
+  std::vector<Node> checkMonomialMagnitude( unsigned c );
+  
+  std::vector<Node> checkMonomialInferBounds( std::vector<Node>& nt_lemmas,
+                                              const std::set<Node>& false_asserts );
+  
+  std::vector<Node> checkFactoring( const std::set<Node>& false_asserts );
+  
+  std::vector<Node> checkMonomialInferResBounds();
+  
+  std::vector<Node> checkTangentPlanes();
+  
+  std::vector<Node> checkTranscendentalInitialRefine();
+
+  std::vector<Node> checkTranscendentalMonotonic();
 }; /* class NonlinearExtension */
 
 }  // namespace arith
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 605dfe495..ef22e1c0d 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -89,6 +89,19 @@ bool Variable::isDivMember(Node n){
   }
 }
 
+bool Variable::isTranscendentalMember(Node n) {
+  switch(n.getKind()){
+  case kind::EXPONENTIAL:
+  case kind::SINE:
+  case kind::COSINE:
+  case kind::TANGENT:
+    return Polynomial::isMember(n[0]);
+  case kind::PI:
+    return true;
+  default:
+    return false;
+  }
+}
 
 
 bool VarList::isSorted(iterator start, iterator end) {
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 4a2b6114f..d8f5259fc 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -245,6 +245,12 @@ public:
     case kind::INTS_MODULUS_TOTAL:
     case kind::DIVISION_TOTAL:
       return isDivMember(n);
+    case kind::EXPONENTIAL:
+    case kind::SINE:
+    case kind::COSINE:
+    case kind::TANGENT:
+    case kind::PI:
+      return isTranscendentalMember(n);      
     case kind::ABS:
     case kind::TO_INTEGER:
       // Treat to_int as a variable; it is replaced in early preprocessing
@@ -260,6 +266,7 @@ public:
   bool isDivLike() const{
     return isDivMember(getNode());
   }
+  static bool isTranscendentalMember(Node n);
 
   bool isNormalForm() { return isMember(getNode()); }
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c0af3827e..985799e88 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -40,6 +40,11 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
   if (options::nlExt()) {
     setupExtTheory();
     getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT);
+    getExtTheory()->addFunctionKind(kind::EXPONENTIAL);
+    getExtTheory()->addFunctionKind(kind::SINE);
+    getExtTheory()->addFunctionKind(kind::COSINE);
+    getExtTheory()->addFunctionKind(kind::TANGENT);
+    getExtTheory()->addFunctionKind(kind::PI);
   }
 }
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c5e8de96a..5fb31e93f 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1454,7 +1454,6 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
     }
 
     if( !options::nlExt() ){
-      setIncomplete();
       d_nlIncomplete = true;
     }
 
@@ -1464,6 +1463,13 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
     //setupInitialValue(av);
 
     markSetup(vlNode);
+  }else{
+    if( !options::nlExt() ){
+      if( vlNode.getKind()==kind::EXPONENTIAL || vlNode.getKind()==kind::SINE || 
+          vlNode.getKind()==kind::COSINE || vlNode.getKind()==kind::TANGENT ){
+        d_nlIncomplete = true;
+      }
+    }
   }
 
   /* Note:
@@ -3823,7 +3829,6 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
   }
 
   if(Theory::fullEffort(effortLevel) && d_nlIncomplete){
-    // TODO this is total paranoia
     setIncomplete();
   }
 
@@ -4865,6 +4870,12 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
 Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) {
   NodeManager* nm = NodeManager::currentNM();
 
+  // eliminate here since involves division
+  if( node.getKind()==kind::TANGENT ){
+    node = nm->mkNode(kind::DIVISION, nm->mkNode( kind::SINE, node[0] ), 
+                                      nm->mkNode( kind::COSINE, node[0] ) );
+  }
+
   switch(node.getKind()) {
   case kind::DIVISION: {
     // partial function: division
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index e13dee0fe..59c2aaa8f 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -93,6 +93,24 @@ public:
   }
 };/* class IntOperatorTypeRule */
 
+class RealOperatorTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TNode::iterator child_it = n.begin();
+    TNode::iterator child_it_end = n.end();
+    if(check) {
+      for(; child_it != child_it_end; ++child_it) {
+        TypeNode childType = (*child_it).getType(check);
+        if (!childType.isReal()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a real subterm");
+        }
+      }
+    }
+    return nodeManager->realType();
+  }
+};/* class RealOperatorTypeRule */
+
 class ArithPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -139,6 +157,21 @@ public:
   }
 };/* class IntUnaryPredicateTypeRule */
 
+class RealNullaryOperatorTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation
+    Assert(check);
+    TypeNode realType = n.getType();
+    if(realType!=NodeManager::currentNM()->realType()) {
+      throw TypeCheckingExceptionPrivate(n, "expecting real type");
+    }
+    return realType;
+  }
+};/* class RealNullaryOperatorTypeRule */
+
+
 class SubrangeProperties {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {
diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index 53e04a1ef..e8bff57bd 100644
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -49,7 +49,22 @@ TESTS =	\
   bug698.smt2  \
   real-div-ufnra.smt2 \
   div-mod-partial.smt2 \
-  all-logic.smt2
+  all-logic.smt2 \
+  nta/bad-050217.smt2 \
+  nta/cos-bound.smt2 \
+  nta/cos-sig-value.smt2 \
+  nta/exp_monotone.smt2 \
+  nta/shifting2.smt2 \
+  nta/shifting.smt2 \
+  nta/sin-compare-across-phase.smt2 \
+  nta/sin-compare.smt2 \
+  nta/sin-sign.smt2 \
+  nta/sin-sym2.smt2 \
+  nta/sin-sym.smt2 \
+  nta/tan-rewrite2.smt2 \
+  nta/tan-rewrite.smt2 \
+  nta/arrowsmith-050317.smt2 \
+  nta/sin-init-tangents.smt2
 
 # unsolved : garbage_collect.cvc
 
diff --git a/test/regress/regress0/nl/nta/arrowsmith-050317.smt2 b/test/regress/regress0/nl/nta/arrowsmith-050317.smt2
new file mode 100644
index 000000000..04b06e1f5
--- /dev/null
+++ b/test/regress/regress0/nl/nta/arrowsmith-050317.smt2
@@ -0,0 +1,95 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun time__AT0@0 () Real)
+(declare-fun instance.location.0__AT0@0 () Bool)
+(declare-fun instance.y__AT0@0 () Real)
+(declare-fun instance.x__AT0@0 () Real)
+(declare-fun instance.location.0__AT0@4 () Bool)
+(declare-fun event_is_timed__AT0@1 () Bool)
+(declare-fun event_is_timed__AT0@0 () Bool)
+(declare-fun instance.location.0__AT0@1 () Bool)
+(declare-fun instance.x__AT0@1 () Real)
+(declare-fun instance.y__AT0@1 () Real)
+(declare-fun instance.EVENT.0__AT0@0 () Bool)
+(declare-fun instance.EVENT.1__AT0@0 () Bool)
+(declare-fun time__AT0@1 () Real)
+(declare-fun event_is_timed__AT0@3 () Bool)
+(declare-fun instance.location.0__AT0@3 () Bool)
+(declare-fun instance.x__AT0@3 () Real)
+(declare-fun instance.y__AT0@3 () Real)
+(declare-fun instance.EVENT.0__AT0@2 () Bool)
+(declare-fun instance.EVENT.1__AT0@2 () Bool)
+(declare-fun time__AT0@3 () Real)
+(declare-fun event_is_timed__AT0@2 () Bool)
+(declare-fun instance.location.0__AT0@2 () Bool)
+(declare-fun instance.x__AT0@2 () Real)
+(declare-fun instance.y__AT0@2 () Real)
+(declare-fun instance.EVENT.0__AT0@1 () Bool)
+(declare-fun instance.EVENT.1__AT0@1 () Bool)
+(declare-fun time__AT0@2 () Real)
+(declare-fun event_is_timed__AT0@4 () Bool)
+(declare-fun instance.x__AT0@4 () Real)
+(declare-fun instance.y__AT0@4 () Real)
+(declare-fun instance.EVENT.0__AT0@3 () Bool)
+(declare-fun instance.EVENT.1__AT0@3 () Bool)
+(declare-fun time__AT0@4 () Real)
+(assert (let ((.def_0 (not instance.EVENT.1__AT0@3))) (let ((.def_1 (not instance.EVENT.0__AT0@3))) (let ((.def_2 (or .def_1 .def_0))) (let ((.def_3 (= event_is_timed__AT0@3 instance.EVENT.1__AT0@3))) (let ((.def_4 (<= time__AT0@3 
+time__AT0@4))) (let ((.def_5 (or .def_0 .def_4))) (let ((.def_6 (and .def_5 .def_3))) (let ((.def_7 (= time__AT0@3 time__AT0@4))) (let ((.def_8 (or instance.EVENT.1__AT0@3 .def_7))) (let ((.def_9 (and .def_8 .def_6))) (let 
+((.def_10 (<= instance.x__AT0@3 0.0))) (let ((.def_11 (not .def_10))) (let ((.def_12 (not instance.location.0__AT0@3))) (let ((.def_13 (and .def_12 .def_11))) (let ((.def_14 (and instance.location.0__AT0@4 .def_13))) (let ((.def_15 
+(= instance.x__AT0@3 instance.x__AT0@4))) (let ((.def_16 (and .def_15 .def_14))) (let ((.def_17 (= instance.y__AT0@3 instance.y__AT0@4))) (let ((.def_18 (and .def_17 .def_16))) (let ((.def_19 (<= instance.y__AT0@3 0.0))) (let 
+((.def_20 (and .def_12 .def_19))) (let ((.def_21 (and instance.location.0__AT0@4 .def_20))) (let ((.def_22 (and .def_15 .def_21))) (let ((.def_23 (and .def_17 .def_22))) (let ((.def_24 (or .def_23 .def_18))) (let ((.def_25 (and 
+.def_7 .def_24))) (let ((.def_26 (or instance.EVENT.1__AT0@3 .def_25))) (let ((.def_27 (not .def_7))) (let ((.def_28 (and .def_15 .def_17))) (let ((.def_29 (or .def_28 .def_27))) (let ((.def_30 (and .def_28 .def_29))) (let 
+((.def_31 (or .def_30 .def_12))) (let ((.def_32 (* (- 1.0) time__AT0@3))) (let ((.def_33 (+ .def_32 time__AT0@4))) (let ((.def_34 (exp .def_33))) (let ((.def_35 (* instance.x__AT0@3 .def_34))) (let ((.def_36 (= instance.x__AT0@4 
+.def_35))) (let ((.def_37 (* 2.0 instance.x__AT0@4))) (let ((.def_38 (* instance.y__AT0@4 .def_37))) (let ((.def_39 (* (- 1.0) .def_38))) (let ((.def_40 (* 2.0 instance.x__AT0@3))) (let ((.def_41 (* instance.y__AT0@3 .def_40))) 
+(let ((.def_42 (* (- 1.0) .def_41))) (let ((.def_43 (+ instance.y__AT0@3 .def_42))) (let ((.def_44 (* .def_43 .def_34))) (let ((.def_45 (* (- 1.0) .def_44))) (let ((.def_46 (+ .def_45 .def_39))) (let ((.def_47 (+ instance.y__AT0@4 
+.def_46))) (let ((.def_48 (= .def_47 0.0))) (let ((.def_49 (and .def_48 .def_36))) (let ((.def_50 (and .def_49 .def_29))) (let ((.def_51 (or instance.location.0__AT0@3 .def_50))) (let ((.def_52 (and .def_51 .def_31))) (let 
+((.def_53 (and .def_52 .def_4))) (let ((.def_54 (= instance.location.0__AT0@4 instance.location.0__AT0@3))) (let ((.def_55 (and .def_54 .def_53))) (let ((.def_56 (or .def_0 .def_55))) (let ((.def_57 (and .def_56 .def_26))) (let 
+((.def_58 (and .def_1 .def_0))) (let ((.def_59 (or .def_58 .def_57))) (let ((.def_60 (and .def_59 .def_9))) (let ((.def_61 (not .def_58))) (let ((.def_62 (and .def_54 .def_15))) (let ((.def_63 (and .def_62 .def_17))) (let ((.def_64 
+(or .def_63 .def_61))) (let ((.def_65 (and .def_64 .def_60))) (let ((.def_66 (not event_is_timed__AT0@3))) (let ((.def_67 (= event_is_timed__AT0@4 .def_66))) (let ((.def_68 (and .def_67 .def_65))) (let ((.def_69 (and .def_68 
+.def_2))) (let ((.def_70 (not instance.EVENT.1__AT0@2))) (let ((.def_71 (not instance.EVENT.0__AT0@2))) (let ((.def_72 (or .def_71 .def_70))) (let ((.def_73 (= event_is_timed__AT0@2 instance.EVENT.1__AT0@2))) (let ((.def_74 (<= 
+time__AT0@2 time__AT0@3))) (let ((.def_75 (or .def_70 .def_74))) (let ((.def_76 (and .def_75 .def_73))) (let ((.def_77 (= time__AT0@2 time__AT0@3))) (let ((.def_78 (or instance.EVENT.1__AT0@2 .def_77))) (let ((.def_79 (and .def_78 
+.def_76))) (let ((.def_80 (<= instance.x__AT0@2 0.0))) (let ((.def_81 (not .def_80))) (let ((.def_82 (not instance.location.0__AT0@2))) (let ((.def_83 (and .def_82 .def_81))) (let ((.def_84 (and instance.location.0__AT0@3 
+.def_83))) (let ((.def_85 (= instance.x__AT0@2 instance.x__AT0@3))) (let ((.def_86 (and .def_85 .def_84))) (let ((.def_87 (= instance.y__AT0@2 instance.y__AT0@3))) (let ((.def_88 (and .def_87 .def_86))) (let ((.def_89 (<= 
+instance.y__AT0@2 0.0))) (let ((.def_90 (and .def_82 .def_89))) (let ((.def_91 (and instance.location.0__AT0@3 .def_90))) (let ((.def_92 (and .def_85 .def_91))) (let ((.def_93 (and .def_87 .def_92))) (let ((.def_94 (or .def_93 
+.def_88))) (let ((.def_95 (and .def_77 .def_94))) (let ((.def_96 (or instance.EVENT.1__AT0@2 .def_95))) (let ((.def_97 (not .def_77))) (let ((.def_98 (and .def_85 .def_87))) (let ((.def_99 (or .def_98 .def_97))) (let ((.def_100 
+(and .def_98 .def_99))) (let ((.def_101 (or .def_100 .def_82))) (let ((.def_102 (* (- 1.0) time__AT0@2))) (let ((.def_103 (+ .def_102 time__AT0@3))) (let ((.def_104 (exp .def_103))) (let ((.def_105 (* instance.x__AT0@2 .def_104))) 
+(let ((.def_106 (= instance.x__AT0@3 .def_105))) (let ((.def_107 (* 2.0 instance.x__AT0@2))) (let ((.def_108 (* instance.y__AT0@2 .def_107))) (let ((.def_109 (* (- 1.0) .def_108))) (let ((.def_110 (+ instance.y__AT0@2 .def_109))) 
+(let ((.def_111 (* .def_110 .def_104))) (let ((.def_112 (* (- 1.0) .def_111))) (let ((.def_113 (+ .def_112 .def_42))) (let ((.def_114 (+ instance.y__AT0@3 .def_113))) (let ((.def_115 (= .def_114 0.0))) (let ((.def_116 (and .def_115 
+.def_106))) (let ((.def_117 (and .def_116 .def_99))) (let ((.def_118 (or instance.location.0__AT0@2 .def_117))) (let ((.def_119 (and .def_118 .def_101))) (let ((.def_120 (and .def_119 .def_74))) (let ((.def_121 (= 
+instance.location.0__AT0@2 instance.location.0__AT0@3))) (let ((.def_122 (and .def_121 .def_120))) (let ((.def_123 (or .def_70 .def_122))) (let ((.def_124 (and .def_123 .def_96))) (let ((.def_125 (and .def_71 .def_70))) (let 
+((.def_126 (or .def_125 .def_124))) (let ((.def_127 (and .def_126 .def_79))) (let ((.def_128 (not .def_125))) (let ((.def_129 (and .def_121 .def_85))) (let ((.def_130 (and .def_129 .def_87))) (let ((.def_131 (or .def_130 
+.def_128))) (let ((.def_132 (and .def_131 .def_127))) (let ((.def_133 (not event_is_timed__AT0@2))) (let ((.def_134 (= event_is_timed__AT0@3 .def_133))) (let ((.def_135 (and .def_134 .def_132))) (let ((.def_136 (and .def_135 
+.def_72))) (let ((.def_137 (not instance.EVENT.1__AT0@1))) (let ((.def_138 (not instance.EVENT.0__AT0@1))) (let ((.def_139 (or .def_138 .def_137))) (let ((.def_140 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_141 
+(<= time__AT0@1 time__AT0@2))) (let ((.def_142 (or .def_137 .def_141))) (let ((.def_143 (and .def_142 .def_140))) (let ((.def_144 (= time__AT0@1 time__AT0@2))) (let ((.def_145 (or instance.EVENT.1__AT0@1 .def_144))) (let ((.def_146 
+(and .def_145 .def_143))) (let ((.def_147 (<= instance.x__AT0@1 0.0))) (let ((.def_148 (not .def_147))) (let ((.def_149 (not instance.location.0__AT0@1))) (let ((.def_150 (and .def_149 .def_148))) (let ((.def_151 (and 
+instance.location.0__AT0@2 .def_150))) (let ((.def_152 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_153 (and .def_152 .def_151))) (let ((.def_154 (= instance.y__AT0@1 instance.y__AT0@2))) (let ((.def_155 (and .def_154 
+.def_153))) (let ((.def_156 (<= instance.y__AT0@1 0.0))) (let ((.def_157 (and .def_149 .def_156))) (let ((.def_158 (and instance.location.0__AT0@2 .def_157))) (let ((.def_159 (and .def_152 .def_158))) (let ((.def_160 (and .def_154 
+.def_159))) (let ((.def_161 (or .def_160 .def_155))) (let ((.def_162 (and .def_144 .def_161))) (let ((.def_163 (or instance.EVENT.1__AT0@1 .def_162))) (let ((.def_164 (not .def_144))) (let ((.def_165 (and .def_152 .def_154))) (let 
+((.def_166 (or .def_165 .def_164))) (let ((.def_167 (and .def_165 .def_166))) (let ((.def_168 (or .def_167 .def_149))) (let ((.def_169 (* (- 1.0) time__AT0@1))) (let ((.def_170 (+ .def_169 time__AT0@2))) (let ((.def_171 (exp 
+.def_170))) (let ((.def_172 (* instance.x__AT0@1 .def_171))) (let ((.def_173 (= instance.x__AT0@2 .def_172))) (let ((.def_174 (* 2.0 instance.x__AT0@1))) (let ((.def_175 (* instance.y__AT0@1 .def_174))) (let ((.def_176 (* (- 1.0) 
+.def_175))) (let ((.def_177 (+ instance.y__AT0@1 .def_176))) (let ((.def_178 (* .def_177 .def_171))) (let ((.def_179 (* (- 1.0) .def_178))) (let ((.def_180 (+ .def_179 .def_109))) (let ((.def_181 (+ instance.y__AT0@2 .def_180))) 
+(let ((.def_182 (= .def_181 0.0))) (let ((.def_183 (and .def_182 .def_173))) (let ((.def_184 (and .def_183 .def_166))) (let ((.def_185 (or instance.location.0__AT0@1 .def_184))) (let ((.def_186 (and .def_185 .def_168))) (let 
+((.def_187 (and .def_186 .def_141))) (let ((.def_188 (= instance.location.0__AT0@1 instance.location.0__AT0@2))) (let ((.def_189 (and .def_188 .def_187))) (let ((.def_190 (or .def_137 .def_189))) (let ((.def_191 (and .def_190 
+.def_163))) (let ((.def_192 (and .def_138 .def_137))) (let ((.def_193 (or .def_192 .def_191))) (let ((.def_194 (and .def_193 .def_146))) (let ((.def_195 (not .def_192))) (let ((.def_196 (and .def_188 .def_152))) (let ((.def_197 
+(and .def_196 .def_154))) (let ((.def_198 (or .def_197 .def_195))) (let ((.def_199 (and .def_198 .def_194))) (let ((.def_200 (not event_is_timed__AT0@1))) (let ((.def_201 (= event_is_timed__AT0@2 .def_200))) (let ((.def_202 (and 
+.def_201 .def_199))) (let ((.def_203 (and .def_202 .def_139))) (let ((.def_204 (not instance.EVENT.1__AT0@0))) (let ((.def_205 (not instance.EVENT.0__AT0@0))) (let ((.def_206 (or .def_205 .def_204))) (let ((.def_207 (= 
+event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_208 (<= time__AT0@0 time__AT0@1))) (let ((.def_209 (or .def_204 .def_208))) (let ((.def_210 (and .def_209 .def_207))) (let ((.def_211 (= time__AT0@0 time__AT0@1))) (let 
+((.def_212 (or instance.EVENT.1__AT0@0 .def_211))) (let ((.def_213 (and .def_212 .def_210))) (let ((.def_214 (<= instance.x__AT0@0 0.0))) (let ((.def_215 (not .def_214))) (let ((.def_216 (not instance.location.0__AT0@0))) (let 
+((.def_217 (and .def_216 .def_215))) (let ((.def_218 (and instance.location.0__AT0@1 .def_217))) (let ((.def_219 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_220 (and .def_219 .def_218))) (let ((.def_221 (= 
+instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_222 (and .def_221 .def_220))) (let ((.def_223 (<= instance.y__AT0@0 0.0))) (let ((.def_224 (and .def_216 .def_223))) (let ((.def_225 (and instance.location.0__AT0@1 .def_224))) 
+(let ((.def_226 (and .def_219 .def_225))) (let ((.def_227 (and .def_221 .def_226))) (let ((.def_228 (or .def_227 .def_222))) (let ((.def_229 (and .def_211 .def_228))) (let ((.def_230 (or instance.EVENT.1__AT0@0 .def_229))) (let 
+((.def_231 (not .def_211))) (let ((.def_232 (and .def_219 .def_221))) (let ((.def_233 (or .def_232 .def_231))) (let ((.def_234 (and .def_232 .def_233))) (let ((.def_235 (or .def_216 .def_234))) (let ((.def_236 (* (- 1.0) 
+time__AT0@0))) (let ((.def_237 (+ .def_236 time__AT0@1))) (let ((.def_238 (exp .def_237))) (let ((.def_239 (* instance.x__AT0@0 .def_238))) (let ((.def_240 (= instance.x__AT0@1 .def_239))) (let ((.def_241 (* 2.0 
+instance.x__AT0@0))) (let ((.def_242 (* instance.y__AT0@0 .def_241))) (let ((.def_243 (* (- 1.0) .def_242))) (let ((.def_244 (+ instance.y__AT0@0 .def_243))) (let ((.def_245 (* .def_244 .def_238))) (let ((.def_246 (* (- 1.0) 
+.def_245))) (let ((.def_247 (+ .def_246 .def_176))) (let ((.def_248 (+ instance.y__AT0@1 .def_247))) (let ((.def_249 (= .def_248 0.0))) (let ((.def_250 (and .def_249 .def_240))) (let ((.def_251 (and .def_250 .def_233))) (let 
+((.def_252 (or instance.location.0__AT0@0 .def_251))) (let ((.def_253 (and .def_252 .def_235))) (let ((.def_254 (and .def_253 .def_208))) (let ((.def_255 (= instance.location.0__AT0@0 instance.location.0__AT0@1))) (let ((.def_256 
+(and .def_255 .def_254))) (let ((.def_257 (or .def_204 .def_256))) (let ((.def_258 (and .def_257 .def_230))) (let ((.def_259 (and .def_205 .def_204))) (let ((.def_260 (or .def_259 .def_258))) (let ((.def_261 (and .def_260 
+.def_213))) (let ((.def_262 (not .def_259))) (let ((.def_263 (and .def_255 .def_219))) (let ((.def_264 (and .def_263 .def_221))) (let ((.def_265 (or .def_264 .def_262))) (let ((.def_266 (and .def_265 .def_261))) (let ((.def_267 
+(not event_is_timed__AT0@0))) (let ((.def_268 (= event_is_timed__AT0@1 .def_267))) (let ((.def_269 (and .def_268 .def_266))) (let ((.def_270 (and .def_269 .def_206))) (let ((.def_271 (= instance.x__AT0@0 (- 1.0)))) (let ((.def_272 
+(= instance.y__AT0@0 1.0))) (let ((.def_273 (and .def_272 .def_271))) (let ((.def_274 (and .def_216 .def_273))) (let ((.def_275 (= time__AT0@0 0.0))) (let ((.def_276 (and .def_275 .def_274))) (let ((.def_277 (and .def_276 .def_270 
+.def_203 .def_136 .def_69 instance.location.0__AT0@4))) 
+.def_277)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/nta/bad-050217.smt2 b/test/regress/regress0/nl/nta/bad-050217.smt2
new file mode 100644
index 000000000..3b9310748
--- /dev/null
+++ b/test/regress/regress0/nl/nta/bad-050217.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: sat
+(set-logic QF_NRA)
+(set-info :status sat)
+(declare-fun time__AT0@0 () Real)
+(declare-fun instance.y__AT0@0 () Real)
+(declare-fun instance.x__AT0@0 () Real)
+(declare-fun instance.x__AT0@1 () Real)
+(declare-fun event_is_timed__AT0@1 () Bool)
+(declare-fun event_is_timed__AT0@0 () Bool)
+(declare-fun instance.EVENT.0__AT0@0 () Bool)
+(declare-fun instance.EVENT.1__AT0@0 () Bool)
+(declare-fun instance.y__AT0@1 () Real)
+(declare-fun time__AT0@1 () Real)
+(assert (let ((.def_0 (<= 0.0 instance.x__AT0@1))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@0))) (let ((.def_3 (not instance.EVENT.0__AT0@0))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_6 (<= time__AT0@0 time__AT0@1))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@0 time__AT0@1))) (let ((.def_10 (or instance.EVENT.1__AT0@0 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) instance.y__AT0@0))) (let ((.def_13 (+ instance.x__AT0@0 .def_12))) (let ((.def_14 (* (- 1.0) time__AT0@0))) (let ((.def_15 (+ .def_14 time__AT0@1))) (let ((.def_16 (exp .def_15))) (let ((.def_17 (* .def_16 .def_13))) (let ((.def_18 (* (- 1.0) .def_17))) (let ((.def_19 (* (- 1.0) instance.y__AT0@1))) (let ((.def_20 (+ .def_19 .def_18))) (let ((.def_21 (+ instance.x__AT0@1 .def_20))) (let ((.def_22 (= .def_21 0.0))) (let ((.def_23 (+ instance.y__AT0@0 instance.x__AT0@0))) (let ((.def_24 (* .def_23 .def_16))) (let ((.def_25 (* (- 1.0) .def_24))) (let ((.def_26 (+ instance.y__AT0@1 .def_25))) (let ((.def_27 (+ instance.x__AT0@1 .def_26))) (let ((.def_28 (= .def_27 0.0))) (let ((.def_29 (and .def_28 .def_22))) (let ((.def_30 (not .def_9))) (let ((.def_31 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_32 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_33 (and .def_32 .def_31))) (let ((.def_34 (or .def_33 .def_30))) (let ((.def_35 (and .def_34 .def_29))) (let ((.def_36 (and .def_35 .def_6))) (let ((.def_37 (or .def_2 .def_36))) (let ((.def_38 (and .def_37 .def_10))) (let ((.def_39 (and .def_3 .def_2))) (let ((.def_40 (or .def_39 .def_38))) (let ((.def_41 (and .def_40 .def_11))) (let ((.def_42 (not .def_39))) (let ((.def_43 (or .def_42 .def_33))) (let ((.def_44 (and .def_43 .def_41))) (let ((.def_45 (not event_is_timed__AT0@0))) (let ((.def_46 (= event_is_timed__AT0@1 .def_45))) (let ((.def_47 (and .def_46 .def_44))) (let ((.def_48 (and .def_47 .def_4))) (let ((.def_49 (= instance.x__AT0@0 1.0))) (let ((.def_50 (= instance.y__AT0@0 0.0))) (let ((.def_51 (and .def_50 .def_49))) (let ((.def_52 (= time__AT0@0 0.0))) (let ((.def_53 (and .def_52 .def_51))) (let ((.def_54 (and .def_53 .def_48 .def_1))) .def_54))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/nta/cos-bound.smt2 b/test/regress/regress0/nl/nta/cos-bound.smt2
new file mode 100644
index 000000000..e19260d63
--- /dev/null
+++ b/test/regress/regress0/nl/nta/cos-bound.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(declare-fun x () Real)
+(assert (> (cos x) 1.0))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/cos-sig-value.smt2 b/test/regress/regress0/nl/nta/cos-sig-value.smt2
new file mode 100644
index 000000000..e1baeed9c
--- /dev/null
+++ b/test/regress/regress0/nl/nta/cos-sig-value.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (not (= (cos 0.0) 1.0)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/dumortier-050317.smt2 b/test/regress/regress0/nl/nta/dumortier-050317.smt2
new file mode 100644
index 000000000..04c498ca0
--- /dev/null
+++ b/test/regress/regress0/nl/nta/dumortier-050317.smt2
@@ -0,0 +1,38 @@
+(set-logic QF_NRA)
+(declare-fun time__AT0@0 () Real)
+(declare-fun instance.y__AT0@0 () Real)
+(declare-fun instance.x__AT0@0 () Real)
+(declare-fun event_is_timed__AT0@3 () Bool)
+(declare-fun instance.EVENT.0__AT0@2 () Bool)
+(declare-fun instance.EVENT.1__AT0@2 () Bool)
+(declare-fun instance.y__AT0@3 () Real)
+(declare-fun instance.x__AT0@3 () Real)
+(declare-fun time__AT0@3 () Real)
+(declare-fun instance.y__AT0@5 () Real)
+(declare-fun event_is_timed__AT0@1 () Bool)
+(declare-fun event_is_timed__AT0@0 () Bool)
+(declare-fun instance.EVENT.0__AT0@0 () Bool)
+(declare-fun instance.EVENT.1__AT0@0 () Bool)
+(declare-fun instance.y__AT0@1 () Real)
+(declare-fun instance.x__AT0@1 () Real)
+(declare-fun time__AT0@1 () Real)
+(declare-fun event_is_timed__AT0@4 () Bool)
+(declare-fun instance.EVENT.0__AT0@3 () Bool)
+(declare-fun instance.EVENT.1__AT0@3 () Bool)
+(declare-fun instance.y__AT0@4 () Real)
+(declare-fun instance.x__AT0@4 () Real)
+(declare-fun time__AT0@4 () Real)
+(declare-fun event_is_timed__AT0@2 () Bool)
+(declare-fun instance.EVENT.0__AT0@1 () Bool)
+(declare-fun instance.EVENT.1__AT0@1 () Bool)
+(declare-fun instance.y__AT0@2 () Real)
+(declare-fun instance.x__AT0@2 () Real)
+(declare-fun time__AT0@2 () Real)
+(declare-fun event_is_timed__AT0@5 () Bool)
+(declare-fun instance.EVENT.0__AT0@4 () Bool)
+(declare-fun instance.EVENT.1__AT0@4 () Bool)
+(declare-fun instance.x__AT0@5 () Real)
+(declare-fun time__AT0@5 () Real)
+(assert (let ((.def_0 (<= instance.y__AT0@5 2.0))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@4))) (let ((.def_3 (not instance.EVENT.0__AT0@4))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@4 instance.EVENT.1__AT0@4))) (let ((.def_6 (<= time__AT0@4 time__AT0@5))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@4 time__AT0@5))) (let ((.def_10 (or instance.EVENT.1__AT0@4 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) time__AT0@4))) (let ((.def_13 (+ .def_12 time__AT0@5))) (let ((.def_14 (exp .def_13))) (let ((.def_15 (* instance.y__AT0@4 .def_14))) (let ((.def_16 (= instance.y__AT0@5 .def_15))) (let ((.def_17 (* 970143.0 instance.x__AT0@5))) (let ((.def_18 (* (- 970143.0) instance.x__AT0@4))) (let ((.def_19 (+ .def_18 .def_17))) (let ((.def_20 (* (- 242536.0) instance.y__AT0@4))) (let ((.def_21 (+ .def_20 .def_19))) (let ((.def_22 (* 242536.0 instance.y__AT0@5))) (let ((.def_23 (+ .def_22 .def_21))) (let ((.def_24 (= .def_23 0.0))) (let ((.def_25 (and .def_24 .def_16))) (let ((.def_26 (not .def_9))) (let ((.def_27 (= instance.x__AT0@4 instance.x__AT0@5))) (let ((.def_28 (= instance.y__AT0@5 instance.y__AT0@4))) (let ((.def_29 (and .def_28 .def_27))) (let ((.def_30 (or .def_29 .def_26))) (let ((.def_31 (and .def_30 .def_25))) (let ((.def_32 (and .def_31 .def_6))) (let ((.def_33 (or .def_2 .def_32))) (let ((.def_34 (and .def_33 .def_10))) (let ((.def_35 (and .def_3 .def_2))) (let ((.def_36 (or .def_35 .def_34))) (let ((.def_37 (and .def_36 .def_11))) (let ((.def_38 (not .def_35))) (let ((.def_39 (or .def_38 .def_29))) (let ((.def_40 (and .def_39 .def_37))) (let ((.def_41 (not event_is_timed__AT0@4))) (let ((.def_42 (= event_is_timed__AT0@5 .def_41))) (let ((.def_43 (and .def_42 .def_40))) (let ((.def_44 (and .def_43 .def_4))) (let ((.def_45 (not instance.EVENT.1__AT0@3))) (let ((.def_46 (not instance.EVENT.0__AT0@3))) (let ((.def_47 (or .def_46 .def_45))) (let ((.def_48 (= event_is_timed__AT0@3 instance.EVENT.1__AT0@3))) (let ((.def_49 (<= time__AT0@3 time__AT0@4))) (let ((.def_50 (or .def_45 .def_49))) (let ((.def_51 (and .def_50 .def_48))) (let ((.def_52 (= time__AT0@3 time__AT0@4))) (let ((.def_53 (or instance.EVENT.1__AT0@3 .def_52))) (let ((.def_54 (and .def_53 .def_51))) (let ((.def_55 (* (- 1.0) time__AT0@3))) (let ((.def_56 (+ .def_55 time__AT0@4))) (let ((.def_57 (exp .def_56))) (let ((.def_58 (* instance.y__AT0@3 .def_57))) (let ((.def_59 (= instance.y__AT0@4 .def_58))) (let ((.def_60 (+ .def_20 .def_18))) (let ((.def_61 (* 970143.0 instance.x__AT0@3))) (let ((.def_62 (+ .def_61 .def_60))) (let ((.def_63 (* 242536.0 instance.y__AT0@3))) (let ((.def_64 (+ .def_63 .def_62))) (let ((.def_65 (= .def_64 0.0))) (let ((.def_66 (and .def_65 .def_59))) (let ((.def_67 (not .def_52))) (let ((.def_68 (= instance.x__AT0@3 instance.x__AT0@4))) (let ((.def_69 (= instance.y__AT0@3 instance.y__AT0@4))) (let ((.def_70 (and .def_69 .def_68))) (let ((.def_71 (or .def_70 .def_67))) (let ((.def_72 (and .def_71 .def_66))) (let ((.def_73 (and .def_72 .def_49))) (let ((.def_74 (or .def_45 .def_73))) (let ((.def_75 (and .def_74 .def_53))) (let ((.def_76 (and .def_46 .def_45))) (let ((.def_77 (or .def_76 .def_75))) (let ((.def_78 (and .def_77 .def_54))) (let ((.def_79 (not .def_76))) (let ((.def_80 (or .def_79 .def_70))) (let ((.def_81 (and .def_80 .def_78))) (let ((.def_82 (not event_is_timed__AT0@3))) (let ((.def_83 (= event_is_timed__AT0@4 .def_82))) (let ((.def_84 (and .def_83 .def_81))) (let ((.def_85 (and .def_84 .def_47))) (let ((.def_86 (not instance.EVENT.1__AT0@2))) (let ((.def_87 (not instance.EVENT.0__AT0@2))) (let ((.def_88 (or .def_87 .def_86))) (let ((.def_89 (= event_is_timed__AT0@2 instance.EVENT.1__AT0@2))) (let ((.def_90 (<= time__AT0@2 time__AT0@3))) (let ((.def_91 (or .def_86 .def_90))) (let ((.def_92 (and .def_91 .def_89))) (let ((.def_93 (= time__AT0@2 time__AT0@3))) (let ((.def_94 (or instance.EVENT.1__AT0@2 .def_93))) (let ((.def_95 (and .def_94 .def_92))) (let ((.def_96 (* (- 1.0) time__AT0@2))) (let ((.def_97 (+ .def_96 time__AT0@3))) (let ((.def_98 (exp .def_97))) (let ((.def_99 (* instance.y__AT0@2 .def_98))) (let ((.def_100 (= instance.y__AT0@3 .def_99))) (let ((.def_101 (* (- 970143.0) instance.x__AT0@3))) (let ((.def_102 (* (- 242536.0) instance.y__AT0@3))) (let ((.def_103 (+ .def_102 .def_101))) (let ((.def_104 (* 970143.0 instance.x__AT0@2))) (let ((.def_105 (+ .def_104 .def_103))) (let ((.def_106 (* 242536.0 instance.y__AT0@2))) (let ((.def_107 (+ .def_106 .def_105))) (let ((.def_108 (= .def_107 0.0))) (let ((.def_109 (and .def_108 .def_100))) (let ((.def_110 (not .def_93))) (let ((.def_111 (= instance.x__AT0@2 instance.x__AT0@3))) (let ((.def_112 (= instance.y__AT0@2 instance.y__AT0@3))) (let ((.def_113 (and .def_112 .def_111))) (let ((.def_114 (or .def_113 .def_110))) (let ((.def_115 (and .def_114 .def_109))) (let ((.def_116 (and .def_115 .def_90))) (let ((.def_117 (or .def_86 .def_116))) (let ((.def_118 (and .def_117 .def_94))) (let ((.def_119 (and .def_87 .def_86))) (let ((.def_120 (or .def_119 .def_118))) (let ((.def_121 (and .def_120 .def_95))) (let ((.def_122 (not .def_119))) (let ((.def_123 (or .def_122 .def_113))) (let ((.def_124 (and .def_123 .def_121))) (let ((.def_125 (not event_is_timed__AT0@2))) (let ((.def_126 (= event_is_timed__AT0@3 .def_125))) (let ((.def_127 (and .def_126 .def_124))) (let ((.def_128 (and .def_127 .def_88))) (let ((.def_129 (not instance.EVENT.1__AT0@1))) (let ((.def_130 (not instance.EVENT.0__AT0@1))) (let ((.def_131 (or .def_130 .def_129))) (let ((.def_132 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_133 (<= time__AT0@1 time__AT0@2))) (let ((.def_134 (or .def_129 .def_133))) (let ((.def_135 (and .def_134 .def_132))) (let ((.def_136 (= time__AT0@1 time__AT0@2))) (let ((.def_137 (or instance.EVENT.1__AT0@1 .def_136))) (let ((.def_138 (and .def_137 .def_135))) (let ((.def_139 (* (- 1.0) time__AT0@1))) (let ((.def_140 (+ .def_139 time__AT0@2))) (let ((.def_141 (exp .def_140))) (let ((.def_142 (* instance.y__AT0@1 .def_141))) (let ((.def_143 (= instance.y__AT0@2 .def_142))) (let ((.def_144 (* (- 970143.0) instance.x__AT0@2))) (let ((.def_145 (* (- 242536.0) instance.y__AT0@2))) (let ((.def_146 (+ .def_145 .def_144))) (let ((.def_147 (* 970143.0 instance.x__AT0@1))) (let ((.def_148 (+ .def_147 .def_146))) (let ((.def_149 (* 242536.0 instance.y__AT0@1))) (let ((.def_150 (+ .def_149 .def_148))) (let ((.def_151 (= .def_150 0.0))) (let ((.def_152 (and .def_151 .def_143))) (let ((.def_153 (not .def_136))) (let ((.def_154 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_155 (= instance.y__AT0@1 instance.y__AT0@2))) (let ((.def_156 (and .def_155 .def_154))) (let ((.def_157 (or .def_156 .def_153))) (let ((.def_158 (and .def_157 .def_152))) (let ((.def_159 (and .def_158 .def_133))) (let ((.def_160 (or .def_129 .def_159))) (let ((.def_161 (and .def_160 .def_137))) (let ((.def_162 (and .def_130 .def_129))) (let ((.def_163 (or .def_162 .def_161))) (let ((.def_164 (and .def_163 .def_138))) (let ((.def_165 (not .def_162))) (let ((.def_166 (or .def_165 .def_156))) (let ((.def_167 (and .def_166 .def_164))) (let ((.def_168 (not event_is_timed__AT0@1))) (let ((.def_169 (= event_is_timed__AT0@2 .def_168))) (let ((.def_170 (and .def_169 .def_167))) (let ((.def_171 (and .def_170 .def_131))) (let ((.def_172 (not instance.EVENT.1__AT0@0))) (let ((.def_173 (not instance.EVENT.0__AT0@0))) (let ((.def_174 (or .def_173 .def_172))) (let ((.def_175 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_176 (<= time__AT0@0 time__AT0@1))) (let ((.def_177 (or .def_172 .def_176))) (let ((.def_178 (and .def_177 .def_175))) (let ((.def_179 (= time__AT0@0 time__AT0@1))) (let ((.def_180 (or instance.EVENT.1__AT0@0 .def_179))) (let ((.def_181 (and .def_180 .def_178))) (let ((.def_182 (* (- 1.0) time__AT0@0))) (let ((.def_183 (+ .def_182 time__AT0@1))) (let ((.def_184 (exp .def_183))) (let ((.def_185 (* instance.y__AT0@0 .def_184))) (let ((.def_186 (= instance.y__AT0@1 .def_185))) (let ((.def_187 (* (- 970143.0) instance.x__AT0@1))) (let ((.def_188 (* (- 242536.0) instance.y__AT0@1))) (let ((.def_189 (+ .def_188 .def_187))) (let ((.def_190 (* 970143.0 instance.x__AT0@0))) (let ((.def_191 (+ .def_190 .def_189))) (let ((.def_192 (* 242536.0 instance.y__AT0@0))) (let ((.def_193 (+ .def_192 .def_191))) (let ((.def_194 (= .def_193 0.0))) (let ((.def_195 (and .def_194 .def_186))) (let ((.def_196 (not .def_179))) (let ((.def_197 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_198 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_199 (and .def_198 .def_197))) (let ((.def_200 (or .def_199 .def_196))) (let ((.def_201 (and .def_200 .def_195))) (let ((.def_202 (and .def_201 .def_176))) (let ((.def_203 (or .def_172 .def_202))) (let ((.def_204 (and .def_203 .def_180))) (let ((.def_205 (and .def_173 .def_172))) (let ((.def_206 (or .def_205 .def_204))) (let ((.def_207 (and .def_206 .def_181))) (let ((.def_208 (not .def_205))) (let ((.def_209 (or .def_208 .def_199))) (let ((.def_210 (and .def_209 .def_207))) (let ((.def_211 (not event_is_timed__AT0@0))) (let ((.def_212 (= event_is_timed__AT0@1 .def_211))) (let ((.def_213 (and .def_212 .def_210))) (let ((.def_214 (and .def_213 .def_174))) (let ((.def_215 (<= instance.x__AT0@0 (- (/ 1 2))))) (let ((.def_216 (not .def_215))) (let ((.def_217 (<= 0.0 instance.x__AT0@0))) (let ((.def_218 (not .def_217))) (let ((.def_219 (and .def_218 .def_216))) (let ((.def_220 (<= 0.0 instance.y__AT0@0))) (let ((.def_221 (not .def_220))) (let ((.def_222 (<= (- (/ 1 2)) instance.y__AT0@0))) (let ((.def_223 (and .def_222 .def_221))) (let ((.def_224 (and .def_223 .def_219))) (let ((.def_225 (= time__AT0@0 0.0))) (let ((.def_226 (and .def_225 .def_224))) (let ((.def_227 (and .def_226 .def_214 .def_171 .def_128 .def_85 .def_44 .def_1))) .def_227)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/nta/exp_monotone.smt2 b/test/regress/regress0/nl/nta/exp_monotone.smt2
new file mode 100644
index 000000000..a1360dc22
--- /dev/null
+++ b/test/regress/regress0/nl/nta/exp_monotone.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+(declare-fun w () Real)
+
+(assert (< x w))
+
+(assert (> (exp x) (exp y)))
+(assert (> (exp y) (exp z)))
+(assert (> (exp z) (exp w)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/shifting.smt2 b/test/regress/regress0/nl/nta/shifting.smt2
new file mode 100644
index 000000000..320c92d58
--- /dev/null
+++ b/test/regress/regress0/nl/nta/shifting.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: sat
+(set-logic QF_NIRA)
+(set-info :status sat)
+(declare-fun pi () Real)
+
+(assert (and (< 3.0 pi) (< pi 3.5)))
+
+(declare-fun y () Real)
+(assert (and (<= (- pi) y) (<= y pi)))
+
+(declare-fun s () Int)
+
+(declare-fun z () Real)
+
+(assert (= z (* 2 pi s)))
+
+(assert (> z 60))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/shifting2.smt2 b/test/regress/regress0/nl/nta/shifting2.smt2
new file mode 100644
index 000000000..c5e805c50
--- /dev/null
+++ b/test/regress/regress0/nl/nta/shifting2.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NIRA)
+(set-info :status unsat)
+(declare-fun pi () Real)
+
+(assert (and (< 3.0 pi) (< pi 3.5)))
+
+(declare-fun y () Real)
+(assert (and (< (- pi) y) (< y pi)))
+
+(declare-fun s () Int)
+
+(declare-fun z () Real)
+
+(assert (= z (+ y (* 2 pi s))))
+
+(assert (and (< (- pi) z) (< z pi)))
+
+(assert (not (= z y)))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2 b/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2
new file mode 100644
index 000000000..f5d7fe32d
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (< (sin 3.1) (sin 3.3)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-compare.smt2 b/test/regress/regress0/nl/nta/sin-compare.smt2
new file mode 100644
index 000000000..790d7037f
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-compare.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (or (> (sin 0.1) (sin 0.2)) (> (sin 6.4) (sin 6.5)))) 
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-init-tangents.smt2 b/test/regress/regress0/nl/nta/sin-init-tangents.smt2
new file mode 100644
index 000000000..e71ab231f
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-init-tangents.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(assert (or (> (sin 0.8) 0.9) (< (sin (- 0.7)) (- 0.75)) (= (sin 3.0) 0.8)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-sign.smt2 b/test/regress/regress0/nl/nta/sin-sign.smt2
new file mode 100644
index 000000000..9b05a3d52
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-sign.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (or (< (sin 0.2) (- 0.1)) (> (sin (- 0.05)) 0.05))) 
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-sym.smt2 b/test/regress/regress0/nl/nta/sin-sym.smt2
new file mode 100644
index 000000000..366906464
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-sym.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (not (= (+ (sin 0.2) (sin (- 0.2))) 0.0)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-sym2.smt2 b/test/regress/regress0/nl/nta/sin-sym2.smt2
new file mode 100644
index 000000000..2e5d4eac2
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-sym2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (and (< 0.0 x) (< x 1.0) (< 0.0 y) (< y 1.0)))
+(assert (= (+ (sin x) (sin y)) 0.0))
+(assert (not (= (+ x y) 0.0)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/tan-rewrite.smt2 b/test/regress/regress0/nl/nta/tan-rewrite.smt2
new file mode 100644
index 000000000..0def70806
--- /dev/null
+++ b/test/regress/regress0/nl/nta/tan-rewrite.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+(assert (= (sin x) 0.24))
+(assert (= (cos x) 0.4))
+(assert (= (tan x) 0.5))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/tan-rewrite2.smt2 b/test/regress/regress0/nl/nta/tan-rewrite2.smt2
new file mode 100644
index 000000000..af39f7559
--- /dev/null
+++ b/test/regress/regress0/nl/nta/tan-rewrite2.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+
+(assert (= (tan x) (sin x)))
+(assert (> (cos x) 0))
+(assert (not (= (cos x) 1)))
+(assert (not (= (sin x) 0)))
+
+(check-sat)
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index aebf0de3b..9bf23f555 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf strings sets sygus sep quantifiers
+SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf nl strings sets sygus sep quantifiers
 
 # don't override a BINARY imported from a personal.mk
 @mk_if@eq ($(BINARY),)
diff --git a/test/regress/regress1/nl/Makefile.am b/test/regress/regress1/nl/Makefile.am
new file mode 100644
index 000000000..a7e4c1411
--- /dev/null
+++ b/test/regress/regress1/nl/Makefile.am
@@ -0,0 +1,31 @@
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	siegel-nl-bases.smt2 \
+	mirko-050417.smt2
+
+EXTRA_DIST = $(TESTS)
+
+# synonyms for "check" in this directory
+.PHONY: regress regress1 test
+regress regress1 test: check
+
+# do nothing in this subdir
+.PHONY: regress0 regress2 regress3 regress4
+regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/nl/mirko-050417.smt2 b/test/regress/regress1/nl/mirko-050417.smt2
new file mode 100644
index 000000000..21fd61f9f
--- /dev/null
+++ b/test/regress/regress1/nl/mirko-050417.smt2
@@ -0,0 +1,74 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun t@0 () Real)
+(declare-fun y2@0 () Real)
+(declare-fun y1@0 () Real)
+(declare-fun t@5 () Real)
+(declare-fun y1@5 () Real)
+(declare-fun y2@5 () Real)
+(declare-fun t@6 () Real)
+(declare-fun y1@6 () Real)
+(declare-fun y2@6 () Real)
+(declare-fun t@1 () Real)
+(declare-fun y1@1 () Real)
+(declare-fun y2@1 () Real)
+(declare-fun t@7 () Real)
+(declare-fun y1@7 () Real)
+(declare-fun y2@7 () Real)
+(declare-fun y1@10 () Real)
+(declare-fun y2@10 () Real)
+(declare-fun t@2 () Real)
+(declare-fun y1@2 () Real)
+(declare-fun y2@2 () Real)
+(declare-fun t@8 () Real)
+(declare-fun y1@8 () Real)
+(declare-fun y2@8 () Real)
+(declare-fun t@3 () Real)
+(declare-fun y1@3 () Real)
+(declare-fun y2@3 () Real)
+(declare-fun t@9 () Real)
+(declare-fun y1@9 () Real)
+(declare-fun y2@9 () Real)
+(declare-fun t@4 () Real)
+(declare-fun y1@4 () Real)
+(declare-fun y2@4 () Real)
+(declare-fun t@10 () Real)
+(assert (let ((.def_0 (<= (- 3.0) y2@10))) (let ((.def_1 (<= y2@10 3.0))) (let ((.def_2 (<= y1@10 3.0))) (let ((.def_3 (<= (- 3.0) y1@10))) (let ((.def_4 (and .def_3 .def_2))) (let ((.def_5 (and .def_4 .def_1))) (let ((.def_6 (and 
+.def_5 .def_0))) (let ((.def_7 (not .def_6))) (let ((.def_8 (cos t@10))) (let ((.def_9 (* (- 2.0) .def_8))) (let ((.def_10 (sin t@10))) (let ((.def_11 (* (- 2.0) .def_10))) (let ((.def_12 (+ .def_11 .def_9))) (let ((.def_13 (+ 
+y2@10 .def_12))) (let ((.def_14 (= .def_13 0.0))) (let ((.def_15 (* 2.0 .def_10))) (let ((.def_16 (+ .def_15 .def_9))) (let ((.def_17 (+ y1@10 .def_16))) (let ((.def_18 (= .def_17 0.0))) (let ((.def_19 (<= t@10 7.0))) (let 
+((.def_20 (* (- 1.0) t@10))) (let ((.def_21 (+ t@9 .def_20))) (let ((.def_22 (= .def_21 (- (/ 1 2))))) (let ((.def_23 (and .def_22 .def_19))) (let ((.def_24 (and .def_23 .def_18))) (let ((.def_25 (and .def_24 .def_14))) (let 
+((.def_26 (* (- 1.0) y2@9))) (let ((.def_27 (cos t@9))) (let ((.def_28 (* 2.0 .def_27))) (let ((.def_29 (+ .def_28 .def_26))) (let ((.def_30 (sin t@9))) (let ((.def_31 (* 2.0 .def_30))) (let ((.def_32 (+ .def_31 .def_29))) (let 
+((.def_33 (= .def_32 0.0))) (let ((.def_34 (* (- 2.0) .def_27))) (let ((.def_35 (+ .def_34 y1@9))) (let ((.def_36 (+ .def_31 .def_35))) (let ((.def_37 (= .def_36 0.0))) (let ((.def_38 (<= t@9 7.0))) (let ((.def_39 (* (- 1.0) t@9))) 
+(let ((.def_40 (+ t@8 .def_39))) (let ((.def_41 (= .def_40 (- (/ 1 2))))) (let ((.def_42 (and .def_41 .def_38))) (let ((.def_43 (and .def_42 .def_37))) (let ((.def_44 (and .def_43 .def_33))) (let ((.def_45 (* (- 1.0) y2@8))) (let 
+((.def_46 (cos t@8))) (let ((.def_47 (* 2.0 .def_46))) (let ((.def_48 (+ .def_47 .def_45))) (let ((.def_49 (sin t@8))) (let ((.def_50 (* 2.0 .def_49))) (let ((.def_51 (+ .def_50 .def_48))) (let ((.def_52 (= .def_51 0.0))) (let 
+((.def_53 (* (- 2.0) .def_46))) (let ((.def_54 (+ .def_53 y1@8))) (let ((.def_55 (+ .def_50 .def_54))) (let ((.def_56 (= .def_55 0.0))) (let ((.def_57 (<= t@8 7.0))) (let ((.def_58 (* (- 1.0) t@8))) (let ((.def_59 (+ t@7 .def_58))) 
+(let ((.def_60 (= .def_59 (- (/ 1 2))))) (let ((.def_61 (and .def_60 .def_57))) (let ((.def_62 (and .def_61 .def_56))) (let ((.def_63 (and .def_62 .def_52))) (let ((.def_64 (* (- 1.0) y2@7))) (let ((.def_65 (cos t@7))) (let 
+((.def_66 (* 2.0 .def_65))) (let ((.def_67 (+ .def_66 .def_64))) (let ((.def_68 (sin t@7))) (let ((.def_69 (* 2.0 .def_68))) (let ((.def_70 (+ .def_69 .def_67))) (let ((.def_71 (= .def_70 0.0))) (let ((.def_72 (* (- 2.0) .def_65))) 
+(let ((.def_73 (+ .def_72 y1@7))) (let ((.def_74 (+ .def_69 .def_73))) (let ((.def_75 (= .def_74 0.0))) (let ((.def_76 (<= t@7 7.0))) (let ((.def_77 (* (- 1.0) t@7))) (let ((.def_78 (+ t@6 .def_77))) (let ((.def_79 (= .def_78 (- (/ 
+1 2))))) (let ((.def_80 (and .def_79 .def_76))) (let ((.def_81 (and .def_80 .def_75))) (let ((.def_82 (and .def_81 .def_71))) (let ((.def_83 (* (- 1.0) y2@6))) (let ((.def_84 (cos t@6))) (let ((.def_85 (* 2.0 .def_84))) (let 
+((.def_86 (+ .def_85 .def_83))) (let ((.def_87 (sin t@6))) (let ((.def_88 (* 2.0 .def_87))) (let ((.def_89 (+ .def_88 .def_86))) (let ((.def_90 (= .def_89 0.0))) (let ((.def_91 (* (- 2.0) .def_84))) (let ((.def_92 (+ .def_91 
+y1@6))) (let ((.def_93 (+ .def_88 .def_92))) (let ((.def_94 (= .def_93 0.0))) (let ((.def_95 (<= t@6 7.0))) (let ((.def_96 (* (- 1.0) t@6))) (let ((.def_97 (+ t@5 .def_96))) (let ((.def_98 (= .def_97 (- (/ 1 2))))) (let ((.def_99 
+(and .def_98 .def_95))) (let ((.def_100 (and .def_99 .def_94))) (let ((.def_101 (and .def_100 .def_90))) (let ((.def_102 (* (- 1.0) y2@5))) (let ((.def_103 (cos t@5))) (let ((.def_104 (* 2.0 .def_103))) (let ((.def_105 (+ .def_104 
+.def_102))) (let ((.def_106 (sin t@5))) (let ((.def_107 (* 2.0 .def_106))) (let ((.def_108 (+ .def_107 .def_105))) (let ((.def_109 (= .def_108 0.0))) (let ((.def_110 (* (- 2.0) .def_103))) (let ((.def_111 (+ .def_110 y1@5))) (let 
+((.def_112 (+ .def_107 .def_111))) (let ((.def_113 (= .def_112 0.0))) (let ((.def_114 (<= t@5 7.0))) (let ((.def_115 (* (- 1.0) t@5))) (let ((.def_116 (+ t@4 .def_115))) (let ((.def_117 (= .def_116 (- (/ 1 2))))) (let ((.def_118 
+(and .def_117 .def_114))) (let ((.def_119 (and .def_118 .def_113))) (let ((.def_120 (and .def_119 .def_109))) (let ((.def_121 (* (- 1.0) y2@4))) (let ((.def_122 (cos t@4))) (let ((.def_123 (* 2.0 .def_122))) (let ((.def_124 (+ 
+.def_123 .def_121))) (let ((.def_125 (sin t@4))) (let ((.def_126 (* 2.0 .def_125))) (let ((.def_127 (+ .def_126 .def_124))) (let ((.def_128 (= .def_127 0.0))) (let ((.def_129 (* (- 2.0) .def_122))) (let ((.def_130 (+ .def_129 
+y1@4))) (let ((.def_131 (+ .def_126 .def_130))) (let ((.def_132 (= .def_131 0.0))) (let ((.def_133 (<= t@4 7.0))) (let ((.def_134 (* (- 1.0) t@4))) (let ((.def_135 (+ t@3 .def_134))) (let ((.def_136 (= .def_135 (- (/ 1 2))))) (let 
+((.def_137 (and .def_136 .def_133))) (let ((.def_138 (and .def_137 .def_132))) (let ((.def_139 (and .def_138 .def_128))) (let ((.def_140 (* (- 1.0) y2@3))) (let ((.def_141 (cos t@3))) (let ((.def_142 (* 2.0 .def_141))) (let 
+((.def_143 (+ .def_142 .def_140))) (let ((.def_144 (sin t@3))) (let ((.def_145 (* 2.0 .def_144))) (let ((.def_146 (+ .def_145 .def_143))) (let ((.def_147 (= .def_146 0.0))) (let ((.def_148 (* (- 2.0) .def_141))) (let ((.def_149 (+ 
+.def_148 y1@3))) (let ((.def_150 (+ .def_145 .def_149))) (let ((.def_151 (= .def_150 0.0))) (let ((.def_152 (<= t@3 7.0))) (let ((.def_153 (* (- 1.0) t@3))) (let ((.def_154 (+ t@2 .def_153))) (let ((.def_155 (= .def_154 (- (/ 1 
+2))))) (let ((.def_156 (and .def_155 .def_152))) (let ((.def_157 (and .def_156 .def_151))) (let ((.def_158 (and .def_157 .def_147))) (let ((.def_159 (* (- 1.0) y2@2))) (let ((.def_160 (cos t@2))) (let ((.def_161 (* 2.0 .def_160))) 
+(let ((.def_162 (+ .def_161 .def_159))) (let ((.def_163 (sin t@2))) (let ((.def_164 (* 2.0 .def_163))) (let ((.def_165 (+ .def_164 .def_162))) (let ((.def_166 (= .def_165 0.0))) (let ((.def_167 (* (- 2.0) .def_160))) (let 
+((.def_168 (+ .def_167 y1@2))) (let ((.def_169 (+ .def_164 .def_168))) (let ((.def_170 (= .def_169 0.0))) (let ((.def_171 (<= t@2 7.0))) (let ((.def_172 (* (- 1.0) t@2))) (let ((.def_173 (+ t@1 .def_172))) (let ((.def_174 (= 
+.def_173 (- (/ 1 2))))) (let ((.def_175 (and .def_174 .def_171))) (let ((.def_176 (and .def_175 .def_170))) (let ((.def_177 (and .def_176 .def_166))) (let ((.def_178 (* (- 1.0) y2@1))) (let ((.def_179 (cos t@1))) (let ((.def_180 (* 
+2.0 .def_179))) (let ((.def_181 (+ .def_180 .def_178))) (let ((.def_182 (sin t@1))) (let ((.def_183 (* 2.0 .def_182))) (let ((.def_184 (+ .def_183 .def_181))) (let ((.def_185 (= .def_184 0.0))) (let ((.def_186 (* (- 2.0) 
+.def_179))) (let ((.def_187 (+ .def_186 y1@1))) (let ((.def_188 (+ .def_183 .def_187))) (let ((.def_189 (= .def_188 0.0))) (let ((.def_190 (<= t@1 7.0))) (let ((.def_191 (* (- 1.0) t@1))) (let ((.def_192 (+ t@0 .def_191))) (let 
+((.def_193 (= .def_192 (- (/ 1 2))))) (let ((.def_194 (and .def_193 .def_190))) (let ((.def_195 (and .def_194 .def_189))) (let ((.def_196 (and .def_195 .def_185))) (let ((.def_197 (= t@0 0.0))) (let ((.def_198 (cos t@0))) (let 
+((.def_199 (* (- 2.0) .def_198))) (let ((.def_200 (+ .def_199 y1@0))) (let ((.def_201 (sin t@0))) (let ((.def_202 (* 2.0 .def_201))) (let ((.def_203 (+ .def_202 .def_200))) (let ((.def_204 (= .def_203 0.0))) (let ((.def_205 (* (- 
+1.0) y2@0))) (let ((.def_206 (* 2.0 .def_198))) (let ((.def_207 (+ .def_206 .def_205))) (let ((.def_208 (+ .def_202 .def_207))) (let ((.def_209 (= .def_208 0.0))) (let ((.def_210 (and .def_209 .def_204))) (let ((.def_211 (and 
+.def_210 .def_197))) (let ((.def_212 (and .def_211 .def_196 .def_177 .def_158 .def_139 .def_120 .def_101 .def_82 .def_63 .def_44 .def_25 .def_7))) 
+.def_212))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/nl/siegel-nl-bases.smt2 b/test/regress/regress1/nl/siegel-nl-bases.smt2
new file mode 100644
index 000000000..cf6e3ab5e
--- /dev/null
+++ b/test/regress/regress1/nl/siegel-nl-bases.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-const n Int)
+(declare-const i1 Int)
+(declare-const i2 Int)
+(declare-const j1 Int)
+(declare-const j2 Int)
+(assert (>= n 0))
+(assert (not (= i1 i2)))
+(assert (<= 0 i1))
+(assert (<= i1 j1))
+(assert (< j1 n))
+(assert (<= 0 i2))
+(assert (<= i2 j2))
+(assert (< j2 n))
+(assert (or
+  (= (+ (* i1 n) j1) (+ (* i2 n) j2))
+  (= (+ (* i1 n) j1) (+ (* j2 n) i2))
+  (= (+ (* j1 n) i1) (+ (* i2 n) j2))
+  (= (+ (* j1 n) i1) (+ (* j2 n) i2))))
+(check-sat)