diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-13 18:48:36 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-13 20:48:36 -0500 |
| commit | 4298cdaa096cd420c87c9af9f20a8b880fe2d25c (patch) | |
| tree | 1ed6e47b9db5691e19a700fd26e1943ba6ea9bad /test/regress/regress1 | |
| parent | 43cec89207dd1043608273769a20309167ad3c90 (diff) | |
Fix fp-bool.sy grammar and require symfpu (#2631)
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/rr-verify/fp-arith.sy | 1 | ||||
| -rw-r--r-- | test/regress/regress1/rr-verify/fp-bool.sy | 3 |
2 files changed, 3 insertions, 1 deletions
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 )) |