Fix equality conflicts reported by FP (#2064)

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 94733b98dc18540a21c84e0bf054b463062512a3..af7e0437fc0919875fdc1a26bf62f3313d45d07e 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -907,8 +907,10 @@ bool TheoryFp::handlePropagation(TNode node) {
 
   bool stat = d_out->propagate(node);
 
-  if (!stat) handleConflict(node);
-
+  if (!stat)
+  {
+    d_conflict = true;
+  }
   return stat;
 }
 

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index d25da1b62e54fbbdd378383fbc043ec7ea785785..182f901ff0d9d1bf12cd0496176db3e47bc70a85 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1557,7 +1557,8 @@ REG1_TESTS = \
        regress1/uflia/microwave21.ec.minimized.smt2 \
        regress1/uflia/simple_cyclic2.smt2 \
        regress1/uflia/speed2_e8_449_e8_517.ec.smt2 \
-       regress1/uflia/stalmark_e7_27_e7_31.ec.smt2
+       regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 \
+       regress1/wrong-qfabvfp-smtcomp2018.smt2
 
 REG2_TESTS = \
        regress2/DTP_k2_n35_c175_s15.smt2 \

diff --git a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
new file mode 100644 (file)
index 0000000..3636b57
--- /dev/null
+++ b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
@@ -0,0 +1,15 @@
+; REQUIRES: symfpu
+; COMMAND-LINE: --decision=internal
+; COMMAND-LINE: --decision=justification
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_BVFP)
+(declare-fun a () (_ BitVec 64))
+(declare-fun b () (_ BitVec 64))
+(assert (fp.leq ((_ to_fp 11 53) a) ((_ to_fp 11 53) (_ bv4626322717216342016 64))))
+(assert (not (fp.isNaN ((_ to_fp 11 53) b))))
+(declare-fun k2 () (_ BitVec 64))
+(assert (or (= k2 b) (= k2 a)))
+(assert
+(or (fp.isNaN ((_ to_fp 11 53) k2)) (fp.gt ((_ to_fp 11 53) k2) ((_ to_fp 11 53) (_ bv4626322717216342016 64))) ))
+(check-sat)
\ No newline at end of file