From 6b46621c4076ace3b0703e29fbdadca04f7635cb Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 19 Dec 2018 11:58:52 -0600
Subject: Fix issues with REWRITE_DONE in floating point rewriter (#2762)

---
 test/regress/CMakeLists.txt                        |  1 +
 .../sygus/temp_input_to_synth_ic-error-121418.sy   | 26 ++++++++++++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy

(limited to 'test/regress')

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)
-- 
cgit v1.2.3