Fix bug for real division.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 4f62f44519831ea8ed52662ca70f63b3adca1f9c..f40e7204ae710f47e8aacfff1abbb2d7f4d6bb8a 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -238,8 +238,8 @@ static Node getSkolemConstrainedToDivisionTotal(
   if(total_div_node.getAttribute(LinearIntDivAttr(), total_div_skolem)) {
     return total_div_skolem;
   }
-  total_div_skolem = nm->mkSkolem("DivisionTotalSkolem", nm->integerType(),
-                                  "the result of an intdiv-by-k term");
+  total_div_skolem = nm->mkSkolem("DivisionTotalSkolem", nm->realType(),
+                                  "the result of a div term");
   total_div_node.setAttribute(LinearIntDivAttr(), total_div_skolem);
   Node zero = mkRationalNode(0);
   Node lemma = den.eqNode(zero).iteNode(
@@ -258,8 +258,8 @@ static Node getSkolemConstrainedToDivision(
   if(div_node.getAttribute(LinearIntDivAttr(), div_skolem)) {
     return div_skolem;
   }
-  div_skolem = nm->mkSkolem("DivisionSkolem", nm->integerType(),
-                            "the result of an intdiv-by-k term");
+  div_skolem = nm->mkSkolem("DivisionSkolem", nm->realType(),
+                            "the result of a div term");
   div_node.setAttribute(LinearIntDivAttr(), div_skolem);
   Node div0 = nm->mkNode(APPLY_UF, div0Func, num);
   Node total_div = getSkolemConstrainedToDivisionTotal(num, den, out);

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

diff --git a/test/regress/regress0/nl/real-div-ufnra.smt2 b/test/regress/regress0/nl/real-div-ufnra.smt2
new file mode 100644 (file)
index 0000000..5e3b32c
--- /dev/null
+++ b/test/regress/regress0/nl/real-div-ufnra.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --nl-ext --simplification=none
+; EXPECT: sat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun f (Real) Real)
+
+(assert (= (f x) 0.2))
+(assert (= (f y) 0.4)) 
+(assert (= (/ (f x) (f y)) 0.5))
+
+(check-sat)