search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
297 stars 52 forks source link

The version of z3 we are currently linking against (tag: z3-4.12.2 from May) again fails to deliver definite answers sometimes #503

Closed quickbeam123 closed 11 months ago

quickbeam123 commented 11 months ago

The issue looks like this:

./vampire_z3_dbg_master_6958 --input_syntax smtlib2 44.smt2 --decode dis-1_1:10_sas=z3:si=on:abs=on:random_seed=6:rtra=on:rawr=on_0 --show_splitting on
[AVATAR] registering a non-splittable: 18. ~leq(add(add(sK0,sK0),add(sK0,add(sK0,sK0))),add(add(add(sK0,sK0),add(sK0,sK0)),add(sK0,sK0))) [cnf transformation 13]
[AVATAR] recomputeModel: + ~1,   - 
[AVATAR] split a clause: 67. s0(s(zero)) = zero | ~leq(X0,s0(s0(s(zero)))) [resolution 63,32]
[AVATAR] recomputeModel: + 2,    - 
[AVATAR] proved 72. ~leq(X0,s0(s0(s(zero)))) <- (2) [avatar component clause 71]
[AVATAR] split a clause: 79. ~leq(X0,s0(s0(s0(s(zero))))) | s0(s0(s(zero))) = zero <- (2) [resolution 72,32]
v5
Condition in file SAT/Z3Interfacing.cpp, line 336 violated:
false
Value of assignment is: (= (s0_$ zero) zero)

on 44.txt

quickbeam123 commented 11 months ago

This could be fixed already in the latest version of z3 (a reason to jump forward). If not, we should probably turn this into a MWE and file a ticket with them...

MichaelRawson commented 11 months ago

I think we're already on the last release (4.12.2) of Z3. I can reproduce the bug, but exporting the log and running the Z3 binary on it says "sat" quite happily. :-/

quickbeam123 commented 11 months ago

Thank you for trying this out, Michael!

I once had a tiny cpp stub program interfacing the z3 api directly and issuing just the necessary calls. I will check out if I can revive it.

Regarding releases, we could also jump to an arbitrary (non-release) commit, but maybe that's not such a great idea...