Hoice fails to generate unsat proof when the backend z3 version is 4.8.8

[moratorium08]

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)
)

[AdrienChampion]

Thank you for your feedback!

z3 4.8.8 does not seem to have been released yet. Did you build z3 by hand? If so, could you provide the exact commit you used so that I can attempt to reproduce the problem?

Thank you for your interest in hoice :)

[moratorium08]

Oh, I'm sorry to use such non-released version of z3. But this bug also occurs with z3 4.8.7(commit id: 30e7c225cd510400eacd41d0a83e013b835a8ece, tag: z3-4.8.7).

[AdrienChampion]

No problem at all that's usually what I do too :D

I will try to look at the problem with z3 4.8.7 shortly and get back to you.

[moratorium08]

Thanks! Actually, I have no problem to use z3-4.8.4, and now I'm using this version. I just wanted to inform other people and developers of the existence of that bug. So, this issue is not an urgent one for me.

[AdrienChampion]

I'm currently not sure what the problem with z3 4.8.7 is. Proof reconstruction fails to generate entry points based on z3's models, i.e. the trace of values that leads to a contradiction cannot be constructed. It might be because z3's models are not actually models, or because of a problem on our end; I haven't investigated enough yet to draw a conclusion.

On more recent versions of z3, including the most recent nightly version at 831afa8, the problem is that z3's models define predicates with quantified tautologies. Typically, ∃ v1!1: Int, v1!1 ≥ 1, which is really true. Unfortunately, hoice expects actual values (of type Bool, here) at this point and parsing fails...

Unfortunately, I don't have a quick solution to this problem :( More work than I can put in right now is needed.

We'll do our best to keep an eye out for this issue and keep you posted, that's currently the best we can do, sorry.