summaryrefslogtreecommitdiff
path: root/test/regress/regress1/rr-verify/fp-bool.sy
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/rr-verify/fp-bool.sy')
-rw-r--r--test/regress/regress1/rr-verify/fp-bool.sy3
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
index 8e404668e..bf0692f7d 100644
--- a/test/regress/regress1/rr-verify/fp-bool.sy
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -1,6 +1,5 @@
-; REQUIRES: no-asan
; 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
+; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
; EXIT: 1
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback