; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --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)