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 with Records #143

Closed DavePearce closed 6 years ago

DavePearce commented 6 years ago

For some reason, this is also causing problems for reasons unknown:

type Point is {int x, int y}

function f(Point p) -> (Point r)
ensures r.x >= 0:
    return p

However, from the command-line, it definitely works. So, unclear why there's a problem.