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/test2/NeverPattern.bpl | 140 ++++++++++++++++++++++---------------------- 1 file changed, 70 insertions(+), 70 deletions(-) (limited to 'Test/test2/NeverPattern.bpl') diff --git a/Test/test2/NeverPattern.bpl b/Test/test2/NeverPattern.bpl index aa301129..5b8fc241 100644 --- a/Test/test2/NeverPattern.bpl +++ b/Test/test2/NeverPattern.bpl @@ -1,70 +1,70 @@ -// RUN: %boogie -noinfer "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -function {:never_pattern true} f1(x:int) returns(int); -function {:never_pattern false} f2(x:int) returns(int); -function f3(x:int) returns(int); - - -procedure foo() -{ - assume (forall x : int :: f1(x) > 0 && f2(x) > 0 && f3(x) > 0); - assert f2(3) > 0; - assert f3(4) > 0; -} - -procedure bar() -{ - assume (forall x : int :: f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); - assert f1(3) > 0; -} - -procedure bar1() -{ - assume (forall x : int :: {:nopats f2(x)} f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); - assert f1(3) > 0; -} - -procedure bar2() -{ - assume (forall x : int :: {:nopats f2(x)} f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); - assert f2(3) > 0; -} - -// ----- nested binders ----- - -function {:never_pattern} P(int): bool; -function F(int, int): int; -function G(int): bool; - -procedure NestedBinders() -{ - goto A, B, C, D; - A: - assume (forall s: int :: - // the occurrence of P in the next line had once caused a crash - (forall x: int :: { F(s, x) } P(F(s, x))) - ==> G(s)); // this places the nested forall in a negative position - goto End; - - B: - assume (forall s: int :: - // the occurrence of P in the next line had once caused a crash - (exists x: int :: { F(s, x) } P(F(s, x)))); - goto End; - - C: - assume (forall s: int, m: [int]bool :: - // the occurrence of P in the next line had once caused a crash - (lambda x: int :: P(F(s, x))) == m); - goto End; - - D: - assume (forall x0: int :: - // The following quantifier will get a {:nopats P(x1,s)}, which is good. - // But that added trigger expression had once caused the outer quantifier - // to crash. - (forall x1: int :: P(x1))); - goto End; - - End: -} +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:never_pattern true} f1(x:int) returns(int); +function {:never_pattern false} f2(x:int) returns(int); +function f3(x:int) returns(int); + + +procedure foo() +{ + assume (forall x : int :: f1(x) > 0 && f2(x) > 0 && f3(x) > 0); + assert f2(3) > 0; + assert f3(4) > 0; +} + +procedure bar() +{ + assume (forall x : int :: f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); + assert f1(3) > 0; +} + +procedure bar1() +{ + assume (forall x : int :: {:nopats f2(x)} f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); + assert f1(3) > 0; +} + +procedure bar2() +{ + assume (forall x : int :: {:nopats f2(x)} f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); + assert f2(3) > 0; +} + +// ----- nested binders ----- + +function {:never_pattern} P(int): bool; +function F(int, int): int; +function G(int): bool; + +procedure NestedBinders() +{ + goto A, B, C, D; + A: + assume (forall s: int :: + // the occurrence of P in the next line had once caused a crash + (forall x: int :: { F(s, x) } P(F(s, x))) + ==> G(s)); // this places the nested forall in a negative position + goto End; + + B: + assume (forall s: int :: + // the occurrence of P in the next line had once caused a crash + (exists x: int :: { F(s, x) } P(F(s, x)))); + goto End; + + C: + assume (forall s: int, m: [int]bool :: + // the occurrence of P in the next line had once caused a crash + (lambda x: int :: P(F(s, x))) == m); + goto End; + + D: + assume (forall x0: int :: + // The following quantifier will get a {:nopats P(x1,s)}, which is good. + // But that added trigger expression had once caused the outer quantifier + // to crash. + (forall x1: int :: P(x1))); + goto End; + + End: +} -- cgit v1.2.3