4 files changed, 89 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 902ddf0f9..aef40d373 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1168,8 +1168,8 @@ set(regress_1_tests
   regress1/nl/dist-big.smt2
   regress1/nl/div-mod-partial.smt2
   regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
-  regress1/nl/exp-approx.smt2
   regress1/nl/exp-4.5-lt.smt2
+  regress1/nl/exp-approx.smt2
   regress1/nl/exp1-lb.smt2
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
@@ -1412,6 +1412,8 @@ set(regress_1_tests
   regress1/rr-verify/bool-crci.sy
   regress1/rr-verify/bv-term-32.sy
   regress1/rr-verify/bv-term.sy
+  regress1/rr-verify/fp-arith.sy
+  regress1/rr-verify/fp-bool.sy
   regress1/rr-verify/regex.sy
   regress1/rr-verify/string-term.sy
   regress1/sep/chain-int.smt2
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 91f33721a..b4e151a17 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1409,6 +1409,8 @@ REG1_TESTS = \
 	regress1/rr-verify/bool-crci.sy \
 	regress1/rr-verify/bv-term-32.sy \
 	regress1/rr-verify/bv-term.sy \
+	regress1/rr-verify/fp-arith.sy \
+	regress1/rr-verify/fp-bool.sy \
 	regress1/rr-verify/regex.sy \
 	regress1/rr-verify/string-term.sy \
 	regress1/sep/chain-int.smt2 \
diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy
new file mode 100644
index 000000000..1b056271c
--- /dev/null
+++ b/test/regress/regress1/rr-verify/fp-arith.sy
@@ -0,0 +1,34 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
+; EXIT: 1
+
+(set-logic FP)
+
+(define-fun fp_plus_zero () Float16 (_ +zero 5 11))
+(define-fun fp_minus_zero () Float16 (_ -zero 5 11))
+(define-fun fp_plus_inf () Float16 (_ +oo 5 11))
+(define-fun fp_minus_inf () Float16 (_ -oo 5 11))
+(define-fun fp_nan () Float16 (_ NaN 5 11))
+
+(synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Float16
+(
+ (Start Float16 (
+  (fp.abs Start)
+  (fp.neg Start)
+  (fp.add r Start Start)
+  (fp.sub r Start Start)
+  (fp.mul r Start Start)
+  (fp.div r Start Start)
+  (fp.sqrt r Start)
+  (fp.rem Start Start)
+  x
+  y
+  fp_plus_zero
+  fp_minus_zero
+  fp_plus_inf
+  fp_minus_inf
+  fp_nan
+ ))
+))
+(check-synth)
diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
new file mode 100644
index 000000000..e94319401
--- /dev/null
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -0,0 +1,50 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
+; EXIT: 1
+
+(set-logic FP)
+
+(define-fun fp_plus_zero () Float16 (_ +zero 5 11))
+(define-fun fp_minus_zero () Float16 (_ -zero 5 11))
+(define-fun fp_plus_inf () Float16 (_ +oo 5 11))
+(define-fun fp_minus_inf () Float16 (_ -oo 5 11))
+(define-fun fp_nan () Float16 (_ NaN 5 11))
+
+(synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Bool
+(
+ (Start Bool (
+  (fp.isNaN FpOp)
+  (fp.isNegative FpOp)
+  (fp.isPositive FpOp)
+  (fp.isZero FpOp)
+  (fp.isSubnormal FpOp)
+  (fp.isNormal FpOp)
+  (and Start Start)
+  (or Start Start)
+  (not Start Start)
+  true
+  false
+ ))
+
+ (FpOp Float16 (
+  (fp.abs FpOp)
+  (fp.neg FpOp)
+  (fp.add r FpOp FpOp)
+  (fp.sub r FpOp FpOp)
+  (fp.mul r FpOp FpOp)
+  (fp.div r FpOp FpOp)
+  (fp.sqrt r FpOp)
+  (fp.rem FpOp FpOp)
+  x
+  y
+  fp_plus_zero
+  fp_minus_zero
+  fp_plus_inf
+  fp_minus_inf
+  fp_nan
+  (ite Start FpOp FpOp)
+ ))
+
+))
+(check-synth)