From 1550a8112d172a37a168b048b5c78642bc39bf90 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Mon, 2 Mar 2015 12:31:28 -0800
Subject: fixed crash reported by Dan. DoModSetAnalysis needs to run before the
 linear and mover type checking.

---
 Test/og/parallel4.bpl.expect | 2 +-
 Test/og/t1.bpl.expect        | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'Test')

diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect
index eaead450..25ad398c 100644
--- a/Test/og/parallel4.bpl.expect
+++ b/Test/og/parallel4.bpl.expect
@@ -1,6 +1,6 @@
 parallel4.bpl(31,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    (0,0): og_init
+    parallel4.bpl(29,5): anon0
     (0,0): anon01
 
 Boogie program verifier finished with 3 verified, 1 error
diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect
index f0195727..0b0c936e 100644
--- a/Test/og/t1.bpl.expect
+++ b/Test/og/t1.bpl.expect
@@ -1,6 +1,5 @@
 t1.bpl(65,5): Error: Non-interference check failed
 Execution trace:
-    (0,0): og_init
     t1.bpl(84,13): anon0
     (0,0): anon05
     (0,0): inline$SetG_1$0$Entry
-- 
cgit v1.2.3