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

Unknown Quantifier Problem #148

Open DavePearce opened 6 years ago

DavePearce commented 6 years ago

The following is failing verification for reasons unknown:

type State is ({int level, bool[] pumps} self)

assert "assertion failed":
    forall(State before):
        if:
            exists(int i):
                (0 <= i) && (i < |before.pumps|)
                (before.pumps[i] == true)           
        then:
            exists(int j):
                (0 <= j) && (j < |before.pumps|)
                (before.pumps[j] == true)
DavePearce commented 6 years ago

Example can be reduced to this:

type State is ({int level, bool[] pumps} self)

assert "assertion failed":
    forall(State before):
        if:
            exists(int i):
                (0 <= i) && (i < |before.pumps|)    
        then:
            exists(int j):
                (0 <= j) && (j < |before.pumps|)