blob: b5d7bff917018657a84b738e42e94068b095a978 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
(set-logic ALL_SUPPORTED)
(declare-var m Int)
(declare-var s Int)
(declare-var inc Int)
(declare-datatypes ((tuple2 0)) ( ((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)
|
