blob: 3519319bd11a25fd5f1c49b7032b148ed9eb5693 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
; 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)
|
