diff options
Diffstat (limited to 'test/regress/regress2/sygus/vcb.sy')
| -rw-r--r-- | test/regress/regress2/sygus/vcb.sy | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy index e6f43fc21..a0122193d 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 --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-repair-const --decision=justification (set-logic LIA) (synth-fun f1 ((x1 Int) (x2 Int)) Int) @@ -10,26 +10,26 @@ (define-fun vmax () Int 2) (define-fun AllZero ((v1 Int) (v2 Int)) Bool - (and (= v1 0) (= v2 0))) + (and (= v1 0) (= v2 0))) (define-fun InV ((v1 Int) (v2 Int)) Bool - (and (and (and (>= v1 vmin) (<= v1 vmax)) (>= v2 vmin)) (<= v2 vmax))) + (and (and (and (>= v1 vmin) (<= v1 vmax)) (>= v2 vmin)) (<= v2 vmax))) (define-fun InVorZero ((v1 Int) (v2 Int)) Bool - (or (InV v1 v2) (AllZero v1 v2))) + (or (InV v1 v2) (AllZero v1 v2))) (define-fun UnsafeSame ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool - (or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1))) - (and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2))))) + (or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1))) + (and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2))))) (define-fun BadSame ((x1 Int) (x2 Int)) Bool - (= x1 x2)) + (= x1 x2)) (define-fun Bad ((x1 Int) (x2 Int)) Bool - (BadSame x1 x2)) + (BadSame x1 x2)) (define-fun Unsafe ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool - (UnsafeSame x1 x2 v1 v2)) + (UnsafeSame x1 x2 v1 v2)) (declare-var x1 Int) @@ -46,8 +46,8 @@ (f2 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2)))))))) (constraint (or (or (or (not (InV v1 v2)) - (Unsafe x1 x2 v1 v2)) - (AllZero (f1 (+ x1 v1) (+ x2 v2)) (f2 (+ x1 v1) (+ x2 v2)))) + (Unsafe x1 x2 v1 v2)) + (AllZero (f1 (+ x1 v1) (+ x2 v2)) (f2 (+ x1 v1) (+ x2 v2)))) (not (AllZero (f1 x1 x2) (f2 x1 x2))))) |