summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-10-09 16:54:58 -0500
committerGitHub <noreply@github.com>2018-10-09 16:54:58 -0500
commit9168f325706e61bb12fec71cd375647e2102f8d3 (patch)
treeaa5129a48322e43ae0f5faa9ade2decbd7091df0 /test
parent90ffa8b4eb26af9060e57be7fe5d6008717d3ce6 (diff)
Support for basic actively-generated enumerators (#2606)
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress1/sygus/trivial-stream.sy2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress1/sygus/trivial-stream.sy b/test/regress/regress1/sygus/trivial-stream.sy
index b8b08d03b..33abb6ee8 100644
--- a/test/regress/regress1/sygus/trivial-stream.sy
+++ b/test/regress/regress1/sygus/trivial-stream.sy
@@ -3,7 +3,7 @@
; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded.")
; EXIT: 1
-; COMMAND-LINE: --sygus-stream --sygus-abort-size=0
+; COMMAND-LINE: --sygus-stream --sygus-abort-size=0 --sygus-active-gen=var-agnostic
(set-logic LIA)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback