From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/bitvectors/bv8.bpl | 50 ++++++++++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 25 deletions(-) (limited to 'Test/bitvectors/bv8.bpl') diff --git a/Test/bitvectors/bv8.bpl b/Test/bitvectors/bv8.bpl index ee572998..557eb4e8 100644 --- a/Test/bitvectors/bv8.bpl +++ b/Test/bitvectors/bv8.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// This file includes some tests for which Boogie once generated bad Z3 input - -procedure foo() -{ - var r: bv3; - var s: bv6; - var u: bv15; - var t: bv24; - - t := t[8: 0] ++ t[10: 0] ++ t[24: 18]; - t := (r ++ s) ++ u; - t := t[16: 0] ++ t[8: 0]; -} - -procedure bar() -{ - var a: bv64; - var b: bv32; - var c: bv8; - - c := a[8:0]; - c := b[8:0]; -} +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// This file includes some tests for which Boogie once generated bad Z3 input + +procedure foo() +{ + var r: bv3; + var s: bv6; + var u: bv15; + var t: bv24; + + t := t[8: 0] ++ t[10: 0] ++ t[24: 18]; + t := (r ++ s) ++ u; + t := t[16: 0] ++ t[8: 0]; +} + +procedure bar() +{ + var a: bv64; + var b: bv32; + var c: bv8; + + c := a[8:0]; + c := b[8:0]; +} -- cgit v1.2.3