Fix issues with REWRITE_DONE in floating point rewriter (#2762)

3 files changed, 37 insertions, 6 deletions

diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index f77291a05..21644161e 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -175,8 +175,9 @@ namespace rewrite {
     if (node[0] == node[1]) {
       return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
     } else if (!isPreRewrite && (node[0] > node[1])) {
-	Node normal = NodeManager::currentNM()->mkNode(kind::EQUAL,node[1],node[0]);
-	return RewriteResponse(REWRITE_DONE, normal);
+      Node normal =
+          NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]);
+      return RewriteResponse(REWRITE_DONE, normal);
     } else {
       return RewriteResponse(REWRITE_DONE, node);
     }
@@ -191,7 +192,7 @@ namespace rewrite {
 	   (k == kind::FLOATINGPOINT_MIN_TOTAL) || (k == kind::FLOATINGPOINT_MAX_TOTAL));
 #endif
     if (node[0] == node[1]) {
-      return RewriteResponse(REWRITE_DONE, node[0]);
+      return RewriteResponse(REWRITE_AGAIN, node[0]);
     } else {
       return RewriteResponse(REWRITE_DONE, node);
     }
@@ -249,7 +250,7 @@ namespace rewrite {
 	(childKind == kind::FLOATINGPOINT_ABS)) {
 
       Node rewritten = NodeManager::currentNM()->mkNode(node.getKind(),node[0][0]);
-      return RewriteResponse(REWRITE_AGAIN, rewritten);
+      return RewriteResponse(REWRITE_AGAIN_FULL, rewritten);
     } else {
       return RewriteResponse(REWRITE_DONE, node);
     } 
@@ -276,8 +277,11 @@ namespace rewrite {
     // Lift negation out of the LHS so it can be cancelled out
     if (working[0].getKind() == kind::FLOATINGPOINT_NEG) {
       NodeManager * nm = NodeManager::currentNM();
-      working = nm->mkNode(kind::FLOATINGPOINT_NEG,
-			   nm->mkNode(kind::FLOATINGPOINT_REM, working[0][0], working[1]));
+      working = nm->mkNode(
+          kind::FLOATINGPOINT_NEG,
+          nm->mkNode(kind::FLOATINGPOINT_REM, working[0][0], working[1]));
+      // in contrast to other rewrites here, this requires rewrite again full
+      return RewriteResponse(REWRITE_AGAIN_FULL, working);
     }
 
     return RewriteResponse(REWRITE_DONE, working);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 95e4b8875..0b196855f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1640,6 +1640,7 @@ set(regress_1_tests
   regress1/sygus/sygus-lambda-fv.sy
   regress1/sygus/sygus-uf-ex.sy
   regress1/sygus/t8.sy
+  regress1/sygus/temp_input_to_synth_ic-error-121418.sy
   regress1/sygus/tl-type-0.sy
   regress1/sygus/tl-type-4x.sy
   regress1/sygus/tl-type.sy
diff --git a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy
new file mode 100644
index 000000000..4efd90314
--- /dev/null
+++ b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy
@@ -0,0 +1,26 @@
+; REQUIRES: symfpu
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(define-sort FP () (_ FloatingPoint 3 5))
+(synth-fun IC ((t FP)) Bool
+  ((Start Bool (
+     true
+     false
+     (fp.isZero StartFP)
+     (ite Start Start Start)
+   ))
+   (StartFP FP (
+     t
+     (fp.sub StartRM StartFP StartFP)
+     (fp.max StartFP StartFP)
+   ))
+   (StartRM RoundingMode
+     (RNE))
+))
+
+(constraint (not (IC (fp #b0 #b110 #b1001) )))
+(constraint (not (IC (fp #b1 #b101 #b1101) )))
+(constraint (not (IC (fp #b1 #b001 #b0110) )))
+(constraint (IC (fp #b0 #b001 #b0001) ))
+(check-synth)