Fix fp-bool.sy grammar and require symfpu (#2631)

diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy
index 1b056271cad91ee2ca75a32abf6205e27f0d902b..cca2487d4ea2e9eaed82570cd7fff5126b854a9d 100644 (file)
--- a/test/regress/regress1/rr-verify/fp-arith.sy
+++ b/test/regress/regress1/rr-verify/fp-arith.sy
@@ -1,3 +1,4 @@
+; REQUIRES: symfpu
 ; 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)'

diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
index e9431940103ca00dbd04f7062efeea9be0f0113e..8792a594c10b22044b11d8b7474b371d1692dfa9 100644 (file)
--- a/test/regress/regress1/rr-verify/fp-bool.sy
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -1,3 +1,4 @@
+; REQUIRES: symfpu
 ; 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)'
@@ -22,7 +23,7 @@
   (fp.isNormal FpOp)
   (and Start Start)
   (or Start Start)
-  (not Start Start)
+  (not Start)
   true
   false
  ))