From b19c840d2bd756d272b8b44c122be809a8b1c633 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 10 Jun 2018 21:43:14 -0500
Subject: [PATCH] Fix equality conflicts reported by FP (#2064)

---
 src/theory/fp/theory_fp.cpp                       |  6 ++++--
 test/regress/Makefile.tests                       |  3 ++-
 .../regress1/wrong-qfabvfp-smtcomp2018.smt2       | 15 +++++++++++++++
 3 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 94733b98d..af7e0437f 100644
--- 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 d25da1b62..182f901ff 100644
--- 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
index 000000000..3636b5795
--- /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
-- 
2.30.2