z3 falsch sagen UNSAT

Question

Für das Problem unten existiert Lösung, aber z3 sagt UNSAT.

(set-logic QF_UFNRA) 
(declare-fun a() Real) 
(declare-fun b() Real) 
(declare-fun c() Real) 
(declare-fun d() Real) 
(declare-fun e() Real) 
(declare-fun f() Real) 
(declare-fun g() Real) 
(declare-fun h() Real) 
(assert (and (<= a 1.0) (> a 0.0))) 
(assert (and (<= b 1.0) (> b 0.0))) 
(assert (and (<= c 1.0) (> c 0.0))) 
(assert (and (<= d 1.0) (> d 0.0))) 
(assert (and (<= e 1.0) (>= e 0.0))) 
(assert (and (<= f 1.0) (>= f 0.0))) 
(assert (and (<= g 1.0) (>= g 0.0))) 
(assert (and (<= h 1.0) (>= h 0.0))) 
(assert (= (* (+ a b) (+ a c)) a)) 
(assert (= (* (+ a b) (+ b d)) b)) 
(assert (= (* (+ a c) (+ c d)) c)) 
(assert (= (* (+ b d) (+ c d)) d)) 
(assert (= (+ a b c d e f g h) 1.0)) 
(check-sat) 

Valid Lösung:

a = 1/12, b = 1/4, c = 1/6, d = 1/2, e = f = g = h = 0 

Ich bin nicht in der Lage, um herauszufinden, warum z3 sagt unsat.

z3-Version ist z3-4.3.0-x64.

Answer 1

Ich weiß nicht, was ist die Version von z3 auf rise4fun (http://rise4fun.com/z3). Ich habe es gerade getestet und es heißt SAT. Es gibt das Modell zurück, das Sie angegeben haben.