diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-08 18:28:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-08 18:28:30 -0500 |
| commit | bd5f6d16dc88624a1dbf463f5d080bdc5af50494 (patch) | |
| tree | b6b49839a60298fb829b61091c5006e30f8ac1ab /test/regress/regress2 | |
| parent | 697c624dec0c292beb0ecb9aae0b01ba54c89473 (diff) | |
Address slow sygus regressions (#2598)
Diffstat (limited to 'test/regress/regress2')
| -rw-r--r-- | test/regress/regress2/sygus/sixfuncs.sy | 83 | ||||
| -rw-r--r-- | test/regress/regress2/sygus/vcb.sy | 2 |
2 files changed, 1 insertions, 84 deletions
diff --git a/test/regress/regress2/sygus/sixfuncs.sy b/test/regress/regress2/sygus/sixfuncs.sy deleted file mode 100644 index fc4d7e5be..000000000 --- a/test/regress/regress2/sygus/sixfuncs.sy +++ /dev/null @@ -1,83 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(set-logic LIA) - -(synth-fun f1 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) - -(synth-fun f2 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (+ Start Start) - ) - ))) - -(synth-fun f3 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) - -(synth-fun f4 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) - -(synth-fun f5 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) - -(synth-fun g1 ((p1 Int) (P1 Int)) Int - ((Start Int ( - p1 - P1 - (- Start Start) - (+ Start Start) - ) - ))) - - -(declare-var x Int) -(declare-var y Int) - -(constraint (= (+ (f1 x y) (f1 x y)) (f2 x y))) -(constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y))) -(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) -(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) - -(constraint (= (- (f1 x y) y) (g1 x y))) - - -(check-synth) - -;; possible solution -;; f1: y+x+1 -;; f2: y+2x+2 -;; f3: y+3x+3 -;; f4: 4y+4x+4 -;; f5: 5y+5x+5 -;; g1: x+1 -;; g2: y+2 -;; g3: y+3 -;; g4: 2y+6 -;; g5: 3y+x+7 - diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy index d8d4ff9bb..e6f43fc21 100644 --- a/test/regress/regress2/sygus/vcb.sy +++ b/test/regress/regress2/sygus/vcb.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --no-sygus-repair-const +; COMMAND-LINE: --sygus-out=status --no-sygus-repair-const --decision=justification (set-logic LIA) (synth-fun f1 ((x1 Int) (x2 Int)) Int) |