diff options
Diffstat (limited to 'test/regress/regress0/sygus/fg_polynomial3.sy')
| -rw-r--r-- | test/regress/regress0/sygus/fg_polynomial3.sy | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/fg_polynomial3.sy b/test/regress/regress0/sygus/fg_polynomial3.sy new file mode 100644 index 000000000..dab92bb88 --- /dev/null +++ b/test/regress/regress0/sygus/fg_polynomial3.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth + +(set-logic LIA) + +(synth-fun addExpr1 ((x Int) (y Int)) Int +) + +(synth-fun addExpr2 ((x Int) (y Int)) Int +) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x (+ x y)))) + +(check-synth) + |