search

vprover / vampire

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

No proof with implies-transitive SMT problem (regression) #563

Closed kazarmy closed 3 months ago

kazarmy commented 3 months ago

With the latest version of Vampire from git (d71672a8c), satisfiability checking for the following SMT problem reaches the 60s time limit with no proof:

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(define-fun conjecture () Bool
    (=> (and (=> p q) (=> q r))
        (=> p r)))
(assert (not conjecture))
(check-sat)

It worked before (proof in < 1s) with Vampire 8d999c135.

kazarmy commented 3 months ago

Forgot to add that the problem is from https://microsoft.github.io/z3guide/docs/logic/propositional-logic.

quickbeam123 commented 3 months ago

Thank you for reporting this! This is 99.9% the same issue as https://github.com/vprover/vampire/issues/561 and @mezpusz is working on a fix. The current workaround is to disable UPDR (via -updr off).

kazarmy commented 3 months ago

Thanks for the quick reply!

kazarmy commented 3 months ago

Closed #563 as completed via dffeeb2541fe71a20f7535c25bcc3df0b302f0ac.