summaryrefslogtreecommitdiff
path: root/test/regress/regress1/rr-verify/bv-term.sy
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/rr-verify/bv-term.sy')
-rw-r--r--test/regress/regress1/rr-verify/bv-term.sy1
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy
index f310396d2..278c10339 100644
--- a/test/regress/regress1/rr-verify/bv-term.sy
+++ b/test/regress/regress1/rr-verify/bv-term.sy
@@ -1,3 +1,4 @@
+; REQUIRES: no-asan
; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break
; COMMAND-LINE: --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check
; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback