diff options
Diffstat (limited to 'test/regress/regress1/sygus/t8.sy')
| -rw-r--r-- | test/regress/regress1/sygus/t8.sy | 41 |
1 files changed, 20 insertions, 21 deletions
diff --git a/test/regress/regress1/sygus/t8.sy b/test/regress/regress1/sygus/t8.sy index 4dd726875..6ac904832 100644 --- a/test/regress/regress1/sygus/t8.sy +++ b/test/regress/regress1/sygus/t8.sy @@ -1,31 +1,30 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(set-logic LIA) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic LIA) ( -synth-fun f_143-17-143-55 ( (x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool - ((Start Bool ( -(< IntExpr IntExpr) -(and Start Start) -(= IntExpr IntExpr) -(not Start ) -(<= IntExpr IntExpr) -(or Start Start) - - - -)) -(IntExpr Int ( -x2 x1 parentNode EMPTY_PARENT -0 1 -)) - - ) +synth-fun f_143-17-143-55 ((x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool +((Start Bool) (IntExpr Int)) +( + (Start Bool ( + (< IntExpr IntExpr) + (and Start Start) + (= IntExpr IntExpr) + (not Start) + (<= IntExpr IntExpr) + (or Start Start) + )) + (IntExpr Int ( + x2 x1 parentNode EMPTY_PARENT + 0 1 + )) +) ) + (declare-var x2_143-17-143-55 Int) (declare-var x1_143-17-143-55 Int) (declare-var parentNode_143-17-143-55 Int) (declare-var EMPTY_PARENT_143-17-143-55 Int) -(constraint (=> (and (= parentNode_143-17-143-55 0) (and (= EMPTY_PARENT_143-17-143-55 -1) (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)) ) ) (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55 ) true))) +(constraint (=> (and (= parentNode_143-17-143-55 0) (and (= EMPTY_PARENT_143-17-143-55 (- 1)) (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)))) (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55) true))) (check-synth) |