diff options
Diffstat (limited to 'test/regress/regress2/sygus/ex23.sy')
| -rw-r--r-- | test/regress/regress2/sygus/ex23.sy | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy index 29e8527dc..9e3d2ea75 100644 --- a/test/regress/regress2/sygus/ex23.sy +++ b/test/regress/regress2/sygus/ex23.sy @@ -1,17 +1,12 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const (set-logic LIA) (synth-inv inv-f ((y Int) (z Int) (c Int))) -(declare-primed-var y Int) -(declare-primed-var z Int) -(declare-primed-var c Int) - (define-fun pre-f ((y Int) (z Int) (c Int)) Bool (and (and (= c 0) (>= y 0)) (and (>= 127 y) (= z (* 36 y))))) - (define-fun trans-f ((y Int) (z Int) (c Int) (y! Int) (z! Int) (c! Int)) Bool (and (and (and (< c 36) (= z! (+ z 1))) (= c! (+ c 1))) (= y! y))) |