diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 18:02:00 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 18:02:00 -0700 |
| commit | 0ae413cae2351cbbb3d7b1113d2a808bfbc1d78d (patch) | |
| tree | e03aa1935c227fc66699d0ac090b56e2be2c0e8e | |
| parent | 0089c318f82941fb7dac46e2f6e9657d77b6610f (diff) | |
do checking
| -rw-r--r-- | test/regress/regress1/rr-verify/fp-bool.sy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy index 9096a57b8..e00f7991d 100644 --- a/test/regress/regress1/rr-verify/fp-bool.sy +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --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 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 |