search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Handle Coefficients for CongruenceClosure #86

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following assertion fails with an exception Need to fix this prexisting bug: 2:

assert:
    forall(int x, int y, int z):
        if:
            y == (2 * x)
            z == (y+2)
        then:
            z == (2 * (x+1))

The problem is in CongruenceClosure and should be relatively easy to fix.

DavePearce commented 7 years ago

(this is related to #40)