blob: 09bdb8b4d028e0f5a6b38d18ced74e2ccd807d34 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
; EXPECT: unsat
; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic ALL_SUPPORTED)
(declare-var m Int)
(declare-var s Int)
(declare-var inc Int)
(declare-datatypes () ( (tuple2 (tuple2 (_m Int) (_s Int))) ))
(synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2)
(constraint (=>
(and (>= m 0) (>= s 0) (< s 3) (> inc 0))
(and (>= (_m (x12 m s inc)) 0) (>= (_s (x12 m s inc)) 0) (< (_s (x12 m s inc)) 3) (= (+ (* (_m (x12 m s inc)) 3) (_s (x12 m s inc))) (+ (+ (* m 3) s) inc)))))
(check-synth)
|