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

Counterexample Generation Internal Failure #145

Open DavePearce opened 6 years ago

DavePearce commented 6 years ago

The following causes a counterexample internal failure for reasons unknown:

type nat is (int n) where n >= 0

function sum(nat[] ns) -> (int r)
ensures r >= 0:
    //
    nat i = 0
    nat m = 0
    //
    while i < |ns|:
        m = m + ns[i]
        i = i - 1
    //
    return m
DavePearce commented 5 years ago

This generates the following exception trace:

java.lang.ClassCastException: wytp.proof.Formula$Quantifier cannot be cast to wyal.lang.WyalFile$Expr$UniversalQuantifier
    at wyal.util.Interpreter.evaluateExpression(Interpreter.java:154)
    at wyal.util.Interpreter.checkTypeInvariants(Interpreter.java:681)
    at wyal.util.Interpreter.evaluateForAll(Interpreter.java:124)
    ...