From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 14 Oct 2018 01:48:36 +0000 (-0700)
Subject: Fix fp-bool.sy grammar and require symfpu (#2631)
X-Git-Tag: cvc5-1.0.0~4426
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4298cdaa096cd420c87c9af9f20a8b880fe2d25c;p=cvc5.git

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 1b056271c..cca2487d4 100644
--- 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 e94319401..8792a594c 100644
--- 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
  ))