diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-03-21 22:33:15 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-21 22:33:15 -0500 |
| commit | 37107284adaad3d24da0ad15cac8c88af444aeef (patch) | |
| tree | d98c5a6bf3608a50e828b129d8d8c45b2c49fc58 /test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy | |
| parent | a507aa5f1904055782e1ba01083faf1fd0fb86f7 (diff) | |
Convert V1 Sygus files to V2. (#4136)
Diffstat (limited to 'test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy')
| -rw-r--r-- | test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy | 38 |
1 files changed, 9 insertions, 29 deletions
diff --git a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy b/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy index 38267c10d..c1d196f60 100644 --- a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy +++ b/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete (set-logic LIA) @@ -189,11 +189,11 @@ ) Bool (let - ((X1 Int top.res.abs_3_a_0)) + ((X1 top.res.abs_3_a_0)) (and (= top.res.abs_10_a_0 (and top.res.abs_9_a_0 (< X1 32767))) (let - ((X2 Bool top.res.abs_11_a_0)) + ((X2 top.res.abs_11_a_0)) (and (= top.usr.OK_a_0 (=> X2 (>= X1 0))) (__node_init_voiture_0 @@ -267,11 +267,11 @@ ) Bool (let - ((X1 Int top.res.abs_3_a_1)) + ((X1 top.res.abs_3_a_1)) (and (= top.res.abs_10_a_1 (and top.res.abs_9_a_1 (< X1 32767))) (let - ((X2 Bool top.res.abs_11_a_1)) + ((X2 top.res.abs_11_a_1)) (and (= top.usr.OK_a_1 (=> X2 (>= X1 0))) (__node_trans_voiture_0 @@ -346,26 +346,6 @@ )) -(declare-primed-var top.usr.m Bool) -(declare-primed-var top.usr.s Bool) -(declare-primed-var top.usr.OK Bool) -(declare-primed-var top.res.init_flag Bool) -(declare-primed-var top.res.abs_0 Bool) -(declare-primed-var top.res.abs_1 Bool) -(declare-primed-var top.res.abs_2 Bool) -(declare-primed-var top.res.abs_3 Int) -(declare-primed-var top.res.abs_4 Int) -(declare-primed-var top.res.abs_5 Int) -(declare-primed-var top.res.abs_6 Bool) -(declare-primed-var top.res.abs_7 Bool) -(declare-primed-var top.res.abs_8 Bool) -(declare-primed-var top.res.abs_9 Bool) -(declare-primed-var top.res.abs_10 Bool) -(declare-primed-var top.res.abs_11 Bool) -(declare-primed-var top.res.inst_3 Bool) -(declare-primed-var top.res.inst_2 Bool) -(declare-primed-var top.res.inst_1 Bool) -(declare-primed-var top.res.inst_0 Bool) (define-fun init ( @@ -392,11 +372,11 @@ ) Bool (let - ((X1 Int top.res.abs_3)) + ((X1 top.res.abs_3)) (and (= top.res.abs_10 (and top.res.abs_9 (< X1 32767))) (let - ((X2 Bool top.res.abs_11)) + ((X2 top.res.abs_11)) (and (= top.usr.OK (=> X2 (>= X1 0))) (__node_init_voiture_0 @@ -472,11 +452,11 @@ ) Bool (let - ((X1 Int top.res.abs_3!)) + ((X1 top.res.abs_3!)) (and (= top.res.abs_10! (and top.res.abs_9! (< X1 32767))) (let - ((X2 Bool top.res.abs_11!)) + ((X2 top.res.abs_11!)) (and (= top.usr.OK! (=> X2 (>= X1 0))) (__node_trans_voiture_0 |