1 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/regress2/sygus/min_IC_1.sy b/test/regress/regress2/sygus/min_IC_1.sy
new file mode 100644
index 000000000..92e171312
--- /dev/null
+++ b/test/regress/regress2/sygus/min_IC_1.sy
@@ -0,0 +1,25 @@
+; REQUIRES: symfpu
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(define-sort FP () (_ FloatingPoint 3 5))
+(define-fun IC ((t FP)) Bool (=> (fp.isInfinite t) (fp.isNegative t)))
+
+(synth-fun simpIC ((t FP)) Bool
+  ((Start Bool (
+     (and Start Start)
+     (not Start)
+
+     (fp.isInfinite StartFP)
+     (fp.isNegative StartFP)
+     
+     (ite Start Start Start)
+   ))
+   (StartFP FP (
+     t
+   ))
+))
+
+(declare-var x FP)
+(constraint (= (simpIC x) (IC x)))
+(check-synth)