Fix bug 698.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index fc700fbdcd9b63cbd8111ee73a4d1290f17a944c..acb44bd43a5c2ab693df61ac2fe4d85c5d008cfb 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4288,8 +4288,7 @@ DeltaRational TheoryArithPrivate::getDeltaValue(TNode n) const throw (DeltaRatio
     return value;
   }
 
-  case kind::MULT:
-  case kind::NONLINEAR_MULT: { // 2+ args
+  case kind::MULT: { // 2+ args
     DeltaRational value(1);
     unsigned variableParts = 0;
     for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {

diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index a422c9045a070c3e832eb38f66cf2bfcf660dd4f..13f5611300ab67dd710f53346bb706e4a5f1a6c1 100644 (file)
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -45,7 +45,8 @@ TESTS =       \
   nl-help-unsat-quant.smt2 \
   metitarski-3-4.smt2 \
   rewriting-sums.smt2 \
-  disj-eval.smt2
+  disj-eval.smt2 \
+  bug698.smt2
 
 # unsolved : garbage_collect.cvc
 

diff --git a/test/regress/regress0/nl/bug698.smt2 b/test/regress/regress0/nl/bug698.smt2
index 4f0d6102b74dee6b2a7dfc100dc89ac259778594..ba7610145042d66e3740620e9ee6d6aa5ce05b41 100644 (file)
--- a/test/regress/regress0/nl/bug698.smt2
+++ b/test/regress/regress0/nl/bug698.smt2
@@ -1,6 +1,8 @@
+; COMMAND-LINE: --incremental --nl-alg --fmf-fun-rlv --no-check-models
 (set-logic UFNIA)
 (set-info :smt-lib-version 2.5)
 
+; EXPECT: sat
 (declare-fun fixedAdd() Int)
 (assert (= fixedAdd (+ 2 (+ 2 (+ 2 0)))))
 (check-sat)
@@ -10,14 +12,17 @@
          0 
          (+ a ($$add$$ a (- b 1)))))
 
+; EXPECT: sat
 (declare-fun variableAdd() Int)
 (assert (= variableAdd ($$add$$ 2 3)))
 (check-sat)
 
+; EXPECT: sat
 (declare-fun fixedTimes() Int)
 (assert (= fixedTimes (* 2 (* 2 (* 2 1)))))
 (check-sat)
         
+; EXPECT: sat
 (define-fun-rec $$pow$$ ((a Int)(b Int)) Int 
     (ite (= b 0) 
          1