diff options
Diffstat (limited to 'test/regress/regress1/sygus/sygus-uf-ex.sy')
| -rw-r--r-- | test/regress/regress1/sygus/sygus-uf-ex.sy | 30 |
1 files changed, 18 insertions, 12 deletions
diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy index 66880eafa..7e1cd80b3 100644 --- a/test/regress/regress1/sygus/sygus-uf-ex.sy +++ b/test/regress/regress1/sygus/sygus-uf-ex.sy @@ -1,18 +1,24 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --uf-ho -(set-logic UFLIA) -(declare-fun uf ( Int ) Int) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho +(set-logic ALL) + +(declare-var uf (-> Int Int)) + (synth-fun f ((x Int) (y Int)) Bool -((Start Bool (true false - (<= IntExpr IntExpr ) - (= IntExpr IntExpr ) - (and Start Start ) - (or Start Start ) - (not Start ))) -(IntExpr Int (0 1 x y - (+ IntExpr IntExpr ) - (- IntExpr IntExpr ))))) + ((Start Bool) (IntExpr Int)) + ((Start Bool (true false + (<= IntExpr IntExpr) + (= IntExpr IntExpr) + (and Start Start) + (or Start Start) + (not Start ))) + (IntExpr Int (0 1 x y + (+ IntExpr IntExpr) + (- IntExpr IntExpr))))) + (declare-var x Int) + (constraint (f (uf x) (uf x))) (constraint (not (f 3 4))) + (check-synth) |