Hoice fails to generate unsat proof when the backend z3 version is 4.8.8 #37
Description
Input: smt2 file
(set-logic HORN)
(set-option :produce-proofs true)
(declare-fun X0 (Int) Bool)
(declare-fun X1 (Int) Bool)
(declare-fun X2 (Int) Bool)
(declare-fun X3 (Int) Bool)
(declare-fun X4 (Int) Bool)
(declare-fun X6 (Int) Bool)
(declare-fun X7 (Int) Bool)
(declare-fun X8 (Int) Bool)
(declare-fun X9 (Int) Bool)
(declare-fun X10 (Int) Bool)
(declare-fun X11 (Int) Bool)
(declare-fun X12 (Int) Bool)
(declare-fun X26 (Int Int) Bool)
(declare-fun X27 (Int Int) Bool)
(declare-fun X28 (Int Int) Bool)
(declare-fun X29 (Int Int) Bool)
(declare-fun X30 (Int Int) Bool)
(assert (forall ((n4 Int)) (=> true (X0 n4))))
(assert (forall ((x63 Int)) (=> (and (X1 x63) (<= x63 0)) false)))
(assert (forall ((tmp64 Int)(x62 Int)) (=> (and (= tmp64 (- 0 x62)) (X3 x62)) (X4 tmp64))))
(assert (forall ((x42 Int)(x61 Int)) (=> (and (X3 x42) (X4 x61)) (X2 x61))))
(assert (forall ((tmp65 Int)(x60 Int)) (=> (and (= tmp65 x60) (X9 x60)) (X30 x60 tmp65))))
(assert (forall ((x59 Int)(z28 Int)) (=> (and (X9 z28) (X12 x59)) (X8 x59))))
(assert (forall ((x58 Int)(z28 Int)) (=> (and (X9 z28) (X11 x58)) (X7 x58))))
(assert (forall ((t39 Int)(x57 Int)(z28 Int)) (=> (and (and (X9 z28) (X11 t39)) (X6 x57)) (X10 x57))))
(assert (forall ((x56 Int)(z7 Int)) (=> (X30 x56 z7) (X11 x56))))
(assert (forall ((t39 Int)(x55 Int)(z7 Int)) (=> (and (X30 t39 z7) (X10 x55)) (X29 x55 z7))))
(assert (forall ((x54 Int)(z7 Int)) (=> (X29 x54 z7) (X11 x54))))
(assert (forall ((t39 Int)(x53 Int)(z7 Int)) (=> (and (X29 t39 z7) (X10 x53)) (X12 x53))))
(assert (forall ((tmp66 Int)(x52 Int)) (=> (and (= tmp66 x52) (and (X0 x52) (> x52 0))) (X28 x52 tmp66))))
(assert (forall ((n4 Int)(x51 Int)) (=> (X28 x51 n4) (X26 x51 n4))))
(assert (forall ((n4 Int)(x50 Int)(z28 Int)) (=> (and (X28 z28 n4) (X27 x50 n4)) (X1 x50))))
(assert (forall ((n4 Int)(x49 Int)) (=> (X26 x49 n4) (X9 x49))))
(assert (forall ((n4 Int)(x48 Int)(z28 Int)) (=> (and (X26 z28 n4) (X8 x48)) (X27 x48 n4))))
(assert (forall ((n4 Int)(x47 Int)(z28 Int)) (=> (and (X26 z28 n4) (X7 x47)) (X3 x47))))
(assert (forall ((n4 Int)(t24 Int)(x46 Int)(z28 Int)) (=> (and (and (X26 z28 n4) (X7 t24)) (X2 x46)) (X6 x46))))
(check-sat)
(get-proof)
Output
unsat
(error "
could not reconstruct entry points
while writing unsat proof
")
Version
Hoice 1.8.1(I manually built hoice. Rust version: rustc 1.39.0 (4560ea788 2019-11-04)
z3 4.8.8
To avoid this bug
When I replaced background z3 4.8.8 for z3 4.8.4, it worked well.
unsat
(
(X0 1)
)