Skip to content

Semantics of autoproving

Autoproving has gotten weaker since VeriPB 2.0. Is this intentional?

Attached is an instance that fails on line 5328

Caused by: Proofgoal 3322 could not be autoproven. Please add an explicit subproof for proofgoal 3322.

However, Proofgoal 3322 is a constraint of the form

ABC >= 26

While the database contains a constraint (with ID 3014) that is

ABC >= 27

VeriPB 2 managed to do this.