summaryrefslogtreecommitdiff
path: root/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-07 20:17:09 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-07 20:17:09 +0100
commitd9ed5e32fd306f0da3fc2a24ec17c81bff1c24fc (patch)
treebbd9777c9ed3a3d16f1b01f44c5d54f6b4678432 /Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
parent5bd01834f018249e5d27350ae3cfdf8dd6896637 (diff)
Enabled prover lit tests.
Diffstat (limited to 'Test/prover/EQ_v2.Eval__v4.Eval_out.bpl')
-rw-r--r--Test/prover/EQ_v2.Eval__v4.Eval_out.bpl2
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
index e53e00b4..24c9d5ea 100644
--- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
+++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -typeEncoding:m -z3multipleErrors %s > %t
+// RUN: %diff %s.expect %t
var v4.Mem: [name][int]int;
var v4.alloc: int;