diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 18:06:32 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 18:06:32 -0700 |
| commit | 3f960e4f3744121efddd19b12806fee660887497 (patch) | |
| tree | 78734e6ba90131e826c8847fd8bdb487b0e6ac99 | |
| parent | 0ae413cae2351cbbb3d7b1113d2a808bfbc1d78d (diff) | |
fix
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
| -rw-r--r-- | test/regress/regress1/rr-verify/fp-arith.sy (renamed from test/regress/regress2/rr-verify/fp-arith.sy) | 4 | ||||
| -rw-r--r-- | test/regress/regress1/rr-verify/fp-bool.sy | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index bdaf83cd7..aef40d373 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1412,6 +1412,7 @@ set(regress_1_tests regress1/rr-verify/bool-crci.sy regress1/rr-verify/bv-term-32.sy regress1/rr-verify/bv-term.sy + regress1/rr-verify/fp-arith.sy regress1/rr-verify/fp-bool.sy regress1/rr-verify/regex.sy regress1/rr-verify/string-term.sy @@ -1707,7 +1708,6 @@ set(regress_2_tests regress2/quantifiers/mutualrec2.cvc regress2/quantifiers/net-policy-no-time.smt2 regress2/quantifiers/nunchaku2309663.nun.min.smt2 - regress2/rr-verify/fp-arith.sy regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 regress2/strings/cmu-dis-0707-3.smt2 regress2/strings/cmu-disagree-0707-dd.smt2 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index ab82042eb..b4e151a17 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1409,6 +1409,7 @@ REG1_TESTS = \ regress1/rr-verify/bool-crci.sy \ regress1/rr-verify/bv-term-32.sy \ regress1/rr-verify/bv-term.sy \ + regress1/rr-verify/fp-arith.sy \ regress1/rr-verify/fp-bool.sy \ regress1/rr-verify/regex.sy \ regress1/rr-verify/string-term.sy \ @@ -1700,7 +1701,6 @@ REG2_TESTS = \ regress2/quantifiers/mutualrec2.cvc \ regress2/quantifiers/net-policy-no-time.smt2 \ regress2/quantifiers/nunchaku2309663.nun.min.smt2 \ - regress2/rr-verify/fp-arith.sy \ regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \ regress2/strings/cmu-dis-0707-3.smt2 \ regress2/strings/cmu-disagree-0707-dd.smt2 \ diff --git a/test/regress/regress2/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy index 62f01dbda..1b056271c 100644 --- a/test/regress/regress2/rr-verify/fp-arith.sy +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -1,6 +1,6 @@ -; 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)' +; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' ; EXIT: 1 (set-logic FP) diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy index e00f7991d..e94319401 100644 --- a/test/regress/regress1/rr-verify/fp-bool.sy +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -1,6 +1,6 @@ ; 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)' +; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' ; EXIT: 1 (set-logic FP) |