diff options
Diffstat (limited to 'test/regress/regress1/sygus/twolets1.sy')
-rw-r--r-- | test/regress/regress1/sygus/twolets1.sy | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/twolets1.sy b/test/regress/regress1/sygus/twolets1.sy new file mode 100644 index 000000000..06d2ecb71 --- /dev/null +++ b/test/regress/regress1/sygus/twolets1.sy @@ -0,0 +1,40 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic LIA) + +;; f1 is x plus 2 ;; f2 is 2x plus 5 + +(define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) + +(synth-fun f1 ((x Int)) Int + ( + (Start Int ( + (let0 Intx CInt CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) + +(synth-fun f2 ((x Int)) Int + ( + (Start Int (x + (let0 Intx Start CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) + + +(declare-var x Int) + +(constraint (= (+ (f1 x)(f2 x)) (+ (+ x x) (+ x 8)))) +(constraint (= (- (f2 x)(f1 x)) (+ x 2))) + +(check-synth) + |