r/o
1
(declare-const a Int)
2
(declare-const b Int)
3
(declare-const c Int)
4
(declare-const d Int)
5
(declare-const e Int)
6
(declare-const f Int)
7
(assert (>= a 0))
8
(assert (>= b 0))
9
(assert (>= c 0))
10
(assert (>= d 0))
11
(assert (>= e 0))
12
(assert (>= f 0))
13
(assert (= 3 (+ e f)))
14
(assert (= 5 (+ b f)))
15
(assert (= 4 (+ c d e)))
16
(assert (= 7 (+ a b d)))
17
(minimize (+ a b c d e f))
18
(check-sat)
19
(get-model)
20