From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 5 Apr 2017 18:32:35 +0000 (-0500)
Subject: Fix bug 698.
X-Git-Tag: cvc5-1.0.0~5843
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c03e334d8d204d4083c4bdf2674d1438fdeab394;p=cvc5.git

Fix bug 698.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index fc700fbdc..acb44bd43 100644
--- 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 a422c9045..13f561130 100644
--- 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 4f0d6102b..ba7610145 100644
--- 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