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

Simplification Bug #140

Closed DavePearce closed 6 years ago

DavePearce commented 6 years ago

The following generates an exception:

define prop(bool r, int x, int y) is:
        r <==> (x <= y)

assert:
    forall(bool r, int x, int y):
        prop(x <= y,x,y)

The error trace produced is:

Exception in thread "main" java.lang.RuntimeException: java.lang.IllegalArgumentException: cannot convert expression to atom: wyal.lang.WyalFile$Expr$LessThanOrEqual
    at wyal.commands.VerifyCommand.compile(VerifyCommand.java:254)
    at wyal.commands.VerifyCommand.execute(VerifyCommand.java:202)
    at wyal.commands.VerifyCommand.execute(VerifyCommand.java:1)
    at wycc.WyMain.main(WyMain.java:105)
Caused by: java.lang.IllegalArgumentException: cannot convert expression to atom: wyal.lang.WyalFile$Expr$LessThanOrEqual
    at wytp.proof.rules.Simplification.simplifyExpression(Simplification.java:436)
       ...
DavePearce commented 6 years ago

Ok, was relatively straightforward.