LogicalExprs.bpl « test1 « Test - debian-boogie - Debian packaging for Boogie

summary refs log tree commit diff

path: root/Test/test1/LogicalExprs.bpl

blob: 028d18f4150b26797dcd69be3922c801ac03a30c (plain)

const P: bool;
const Q: bool;

axiom (forall x: int :: x < 0);
axiom Q ==> P;
axiom (forall x: int :: x < 0) ==> P;