From 124d1cee315b79585f7738deb6d72579578d24e2 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 13 Feb 2020 07:22:26 -0800 Subject: [PATCH] Remove typeEncoding:n (#194) The typeEncoding:n option is unsound, as indicated in its documentation. It also does not appear to be used. This commit eliminates the /typeEncoding:n option. --- Source/Core/CommandLineOptions.cs | 6 ----- Source/VCExpr/TypeErasure.cs | 8 +------ Source/VCExpr/TypeErasurePremisses.cs | 19 ++------------- Test/test21/BooleanQuantification.bpl | 4 +--- .../test21/BooleanQuantification.bpl.a.expect | 8 +++---- .../test21/BooleanQuantification.bpl.n.expect | 8 ------- .../test21/BooleanQuantification.bpl.p.expect | 8 +++---- Test/test21/BooleanQuantification2.bpl | 4 +--- .../BooleanQuantification2.bpl.a.expect | 4 ++-- .../BooleanQuantification2.bpl.n.expect | 5 ---- .../BooleanQuantification2.bpl.p.expect | 4 ++-- Test/test21/Boxing.bpl | 4 +--- Test/test21/Boxing.bpl.a.expect | 4 ++-- Test/test21/Boxing.bpl.n.expect | 8 ------- Test/test21/Boxing.bpl.p.expect | 4 ++-- Test/test21/Casts.bpl | 4 +--- Test/test21/Casts.bpl.a.expect | 4 ++-- Test/test21/Casts.bpl.n.expect | 5 ---- Test/test21/Casts.bpl.p.expect | 4 ++-- Test/test21/Coercions2.bpl | 4 +--- Test/test21/Coercions2.bpl.a.expect | 6 ++--- Test/test21/Coercions2.bpl.n.expect | 9 ------- Test/test21/Coercions2.bpl.p.expect | 6 ++--- Test/test21/Colors.bpl | 4 +--- Test/test21/Colors.bpl.a.expect | 8 +++---- Test/test21/Colors.bpl.n.expect | 8 ------- Test/test21/Colors.bpl.p.expect | 8 +++---- Test/test21/DisjointDomains.bpl | 2 -- Test/test21/DisjointDomains.bpl.a.expect | 12 +++++----- Test/test21/DisjointDomains.bpl.n.expect | 2 -- Test/test21/DisjointDomains.bpl.p.expect | 12 +++++----- Test/test21/DisjointDomains2.bpl | 2 -- Test/test21/DisjointDomains2.bpl.a.expect | 24 +++++++++---------- Test/test21/DisjointDomains2.bpl.n.expect | 8 ------- Test/test21/DisjointDomains2.bpl.p.expect | 24 +++++++++---------- Test/test21/EmptyList.bpl | 4 +--- Test/test21/EmptyList.bpl.a.expect | 6 ++--- Test/test21/EmptyList.bpl.n.expect | 12 ---------- Test/test21/EmptyList.bpl.p.expect | 6 ++--- Test/test21/EmptySetBug.bpl | 2 -- Test/test21/EmptySetBug.bpl.a.expect | 4 ++-- Test/test21/EmptySetBug.bpl.n.expect | 8 ------- Test/test21/EmptySetBug.bpl.p.expect | 4 ++-- Test/test21/Flattening.bpl | 4 +--- Test/test21/Flattening.bpl.a.expect | 4 ++-- Test/test21/Flattening.bpl.n.expect | 5 ---- Test/test21/Flattening.bpl.p.expect | 4 ++-- Test/test21/FunAxioms.bpl | 4 +--- Test/test21/FunAxioms.bpl.a.expect | 4 ++-- Test/test21/FunAxioms.bpl.n.expect | 5 ---- Test/test21/FunAxioms.bpl.p.expect | 4 ++-- Test/test21/FunAxioms2.bpl | 4 +--- Test/test21/FunAxioms2.bpl.a.expect | 4 ++-- Test/test21/FunAxioms2.bpl.n.expect | 5 ---- Test/test21/FunAxioms2.bpl.p.expect | 4 ++-- Test/test21/HeapAbstraction.bpl | 2 -- Test/test21/HeapAbstraction.bpl.a.expect | 4 ++-- Test/test21/HeapAbstraction.bpl.n.expect | 2 -- Test/test21/HeapAbstraction.bpl.p.expect | 4 ++-- Test/test21/HeapAxiom.bpl | 2 -- Test/test21/HeapAxiom.bpl.a.expect | 4 ++-- Test/test21/HeapAxiom.bpl.n.expect | 5 ---- Test/test21/HeapAxiom.bpl.p.expect | 4 ++-- Test/test21/InterestingExamples0.bpl | 4 +--- Test/test21/InterestingExamples0.bpl.n.expect | 5 ---- Test/test21/InterestingExamples1.bpl | 2 -- Test/test21/InterestingExamples1.bpl.a.expect | 4 ++-- Test/test21/InterestingExamples1.bpl.n.expect | 8 ------- Test/test21/InterestingExamples1.bpl.p.expect | 4 ++-- Test/test21/InterestingExamples2.bpl | 2 -- Test/test21/InterestingExamples2.bpl.n.expect | 8 ------- Test/test21/InterestingExamples3.bpl | 2 -- Test/test21/InterestingExamples3.bpl.a.expect | 4 ++-- Test/test21/InterestingExamples3.bpl.n.expect | 5 ---- Test/test21/InterestingExamples3.bpl.p.expect | 4 ++-- Test/test21/InterestingExamples4.bpl | 2 -- Test/test21/InterestingExamples4.bpl.a.expect | 8 +++---- Test/test21/InterestingExamples4.bpl.n.expect | 8 ------- Test/test21/InterestingExamples4.bpl.p.expect | 4 ++-- Test/test21/InterestingExamples5.bpl | 4 +--- Test/test21/InterestingExamples5.bpl.n.expect | 2 -- Test/test21/Keywords.bpl | 4 +--- Test/test21/Keywords.bpl.n.expect | 2 -- Test/test21/LargeLiterals0.bpl | 4 +--- Test/test21/LargeLiterals0.bpl.a.expect | 4 ++-- Test/test21/LargeLiterals0.bpl.n.expect | 5 ---- Test/test21/LargeLiterals0.bpl.p.expect | 4 ++-- Test/test21/LetSorting.bpl | 2 -- Test/test21/LetSorting.bpl.n.expect | 2 -- Test/test21/MapAxiomsConsistency.bpl | 2 -- Test/test21/MapAxiomsConsistency.bpl.a.expect | 4 ++-- Test/test21/MapAxiomsConsistency.bpl.n.expect | 5 ---- Test/test21/MapAxiomsConsistency.bpl.p.expect | 4 ++-- Test/test21/MapOutputTypeParams.bpl | 4 +--- Test/test21/MapOutputTypeParams.bpl.a.expect | 14 +++++------ Test/test21/MapOutputTypeParams.bpl.n.expect | 21 ---------------- Test/test21/MapOutputTypeParams.bpl.p.expect | 14 +++++------ Test/test21/Maps0.bpl | 4 +--- Test/test21/Maps0.bpl.a.expect | 12 +++++----- Test/test21/Maps0.bpl.n.expect | 17 ------------- Test/test21/Maps0.bpl.p.expect | 12 +++++----- Test/test21/Maps1.bpl | 2 -- Test/test21/Maps1.bpl.a.expect | 4 ++-- Test/test21/Maps1.bpl.n.expect | 8 ------- Test/test21/Maps1.bpl.p.expect | 4 ++-- Test/test21/Maps2.bpl | 2 -- Test/test21/NameClash.bpl | 4 +--- Test/test21/NameClash.bpl.n.expect | 2 -- Test/test21/Orderings.bpl | 4 +--- Test/test21/Orderings.bpl.a.expect | 4 ++-- Test/test21/Orderings.bpl.n.expect | 5 ---- Test/test21/Orderings.bpl.p.expect | 4 ++-- Test/test21/Orderings2.bpl | 4 +--- Test/test21/Orderings2.bpl.a.expect | 4 ++-- Test/test21/Orderings2.bpl.n.expect | 5 ---- Test/test21/Orderings2.bpl.p.expect | 4 ++-- Test/test21/Orderings3.bpl | 6 ++--- Test/test21/Orderings3.bpl.a.expect | 12 +++++----- Test/test21/Orderings3.bpl.n.expect | 11 --------- Test/test21/Orderings3.bpl.p.expect | 12 +++++----- Test/test21/Orderings4.bpl | 4 +--- Test/test21/Orderings4.bpl.a.expect | 4 ++-- Test/test21/Orderings4.bpl.n.expect | 5 ---- Test/test21/Orderings4.bpl.p.expect | 4 ++-- Test/test21/ParallelAssignment.bpl | 4 +--- Test/test21/ParallelAssignment.bpl.a.expect | 12 +++++----- Test/test21/ParallelAssignment.bpl.n.expect | 11 --------- Test/test21/ParallelAssignment.bpl.p.expect | 12 +++++----- Test/test21/PolyList.bpl | 4 +--- Test/test21/PolyList.bpl.a.expect | 8 +++---- Test/test21/PolyList.bpl.n.expect | 8 ------- Test/test21/PolyList.bpl.p.expect | 8 +++---- Test/test21/Real.bpl | 4 +--- Test/test21/Real.bpl.a.expect | 12 +++++----- Test/test21/Real.bpl.n.expect | 10 -------- Test/test21/Real.bpl.p.expect | 12 +++++----- Test/test21/Triggers0.bpl | 4 +--- Test/test21/Triggers0.bpl.a.expect | 8 +++---- Test/test21/Triggers0.bpl.n.expect | 8 ------- Test/test21/Triggers0.bpl.p.expect | 8 +++---- Test/test21/Triggers1.bpl | 4 +--- Test/test21/Triggers1.bpl.a.expect | 4 ++-- Test/test21/Triggers1.bpl.n.expect | 2 -- Test/test21/Triggers1.bpl.p.expect | 4 ++-- Test/test21/test3_AddMethod_conv.bpl | 2 -- 145 files changed, 250 insertions(+), 615 deletions(-) delete mode 100644 Test/test21/BooleanQuantification.bpl.n.expect delete mode 100644 Test/test21/BooleanQuantification2.bpl.n.expect delete mode 100644 Test/test21/Boxing.bpl.n.expect delete mode 100644 Test/test21/Casts.bpl.n.expect delete mode 100644 Test/test21/Coercions2.bpl.n.expect delete mode 100644 Test/test21/Colors.bpl.n.expect delete mode 100644 Test/test21/DisjointDomains.bpl.n.expect delete mode 100644 Test/test21/DisjointDomains2.bpl.n.expect delete mode 100644 Test/test21/EmptyList.bpl.n.expect delete mode 100644 Test/test21/EmptySetBug.bpl.n.expect delete mode 100644 Test/test21/Flattening.bpl.n.expect delete mode 100644 Test/test21/FunAxioms.bpl.n.expect delete mode 100644 Test/test21/FunAxioms2.bpl.n.expect delete mode 100644 Test/test21/HeapAbstraction.bpl.n.expect delete mode 100644 Test/test21/HeapAxiom.bpl.n.expect delete mode 100644 Test/test21/InterestingExamples0.bpl.n.expect delete mode 100644 Test/test21/InterestingExamples1.bpl.n.expect delete mode 100644 Test/test21/InterestingExamples2.bpl.n.expect delete mode 100644 Test/test21/InterestingExamples3.bpl.n.expect delete mode 100644 Test/test21/InterestingExamples4.bpl.n.expect delete mode 100644 Test/test21/InterestingExamples5.bpl.n.expect delete mode 100644 Test/test21/Keywords.bpl.n.expect delete mode 100644 Test/test21/LargeLiterals0.bpl.n.expect delete mode 100644 Test/test21/LetSorting.bpl.n.expect delete mode 100644 Test/test21/MapAxiomsConsistency.bpl.n.expect delete mode 100644 Test/test21/MapOutputTypeParams.bpl.n.expect delete mode 100644 Test/test21/Maps0.bpl.n.expect delete mode 100644 Test/test21/Maps1.bpl.n.expect delete mode 100644 Test/test21/NameClash.bpl.n.expect delete mode 100644 Test/test21/Orderings.bpl.n.expect delete mode 100644 Test/test21/Orderings2.bpl.n.expect delete mode 100644 Test/test21/Orderings3.bpl.n.expect delete mode 100644 Test/test21/Orderings4.bpl.n.expect delete mode 100644 Test/test21/ParallelAssignment.bpl.n.expect delete mode 100644 Test/test21/PolyList.bpl.n.expect delete mode 100644 Test/test21/Real.bpl.n.expect delete mode 100644 Test/test21/Triggers0.bpl.n.expect delete mode 100644 Test/test21/Triggers1.bpl.n.expect diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index dc3535b9c..c6bcd2618 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -792,7 +792,6 @@ public enum FixedPointInferenceMode { public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically) public enum TypeEncoding { - None, Predicates, Arguments, Monomorphic @@ -1388,10 +1387,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command case "typeEncoding": if (ps.ConfirmArgumentCount(1)) { switch (args[ps.i]) { - case "n": - case "none": - TypeEncodingMethod = TypeEncoding.None; - break; case "p": case "predicates": TypeEncodingMethod = TypeEncoding.Predicates; @@ -2098,7 +2093,6 @@ on stratified inlining. Translate Boogie's A ==> B into prover's A ==> A && B. /typeEncoding: how to encode types when sending VC to theorem prover - n = none (unsound) p = predicates (default) a = arguments m = monomorphic diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index fe436a65c..c79ce0a5a 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -197,10 +197,7 @@ public VCExpr GetNewAxioms() { private VCExpr GenCtorAssignment(VCExpr typeRepr) { Contract.Requires(typeRepr != null); Contract.Ensures(Contract.Result() != null); - if (CommandLineOptions.Clo.TypeEncodingMethod - == CommandLineOptions.TypeEncoding.None) - return VCExpressionGenerator.True; - + VCExpr res = Gen.Eq(Gen.Function(Ctor, typeRepr), Gen.Integer(CurrentCtorNum)); CurrentCtorNum = CurrentCtorNum + BigNum.ONE; @@ -210,9 +207,6 @@ private VCExpr GenCtorAssignment(VCExpr typeRepr) { private VCExpr GenCtorAssignment(Function typeRepr) { Contract.Requires(typeRepr != null); Contract.Ensures(Contract.Result() != null); - if (CommandLineOptions.Clo.TypeEncodingMethod - == CommandLineOptions.TypeEncoding.None) - return VCExpressionGenerator.True; List/*!*/ quantifiedVars = HelperFuns.GenVarsForInParams(typeRepr, Gen); VCExpr/*!*/ eq = diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index dc9ad10f5..6d39ed7ff 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -111,11 +111,7 @@ protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFro Contract.Assert(var != null); Contract.Assert(eq != null); VCExpr/*!*/ premiss; - if (CommandLineOptions.Clo.TypeEncodingMethod - == CommandLineOptions.TypeEncoding.None) - premiss = VCExpressionGenerator.True; - else - premiss = GenVarTypeAxiom(var, cce.NonNull(castFromU.OutParams[0]).TypedIdent.Type, + premiss = GenVarTypeAxiom(var, cce.NonNull(castFromU.OutParams[0]).TypedIdent.Type, // we don't have any bindings available new Dictionary()); VCExpr/*!*/ matrix = Gen.ImpliesSimp(premiss, eq); @@ -436,10 +432,6 @@ private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) { Contract.Requires(originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Count); Contract.Ensures(Contract.Result() != null); - if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) { - return VCExpressionGenerator.True; - } - List/*!*/ typedInputVars = new List(originalInTypes.Count); int i = 0; foreach (Type/*!*/ t in originalInTypes) { @@ -501,7 +493,6 @@ private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) { protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) { //Contract.Requires(originalType != null); //Contract.Requires(var != null); - if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) return; AddTypeAxiom(GenVarTypeAxiom(var, originalType, // we don't have any bindings available new Dictionary())); @@ -841,8 +832,7 @@ private VCExpr GenMapAxiom0(Function select, Function store, Type mapResult, Lis AxBuilderPremisses.Type2Term(mapResult, bindings.TypeVariableBindings)); Contract.Assert(ante != null); VCExpr body; - if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None || - !AxBuilder.U.Equals(cce.NonNull(select.OutParams[0]).TypedIdent.Type)) { + if (!AxBuilder.U.Equals(cce.NonNull(select.OutParams[0]).TypedIdent.Type)) { body = Gen.Let(letBindings_Explicit, eq); } else { body = Gen.Let(letBindings_Implicit, Gen.Let(letBindings_Explicit, Gen.ImpliesSimp(ante, eq))); @@ -1152,11 +1142,6 @@ private VCExpr HandleQuantifier(VCExprQuantifier node, List/*!*/ // assemble the new quantified formula - if (CommandLineOptions.Clo.TypeEncodingMethod - == CommandLineOptions.TypeEncoding.None) { - typePremisses = VCExpressionGenerator.True; - } - VCExpr/*!*/ bodyWithPremisses = AxBuilderPremisses.AddTypePremisses(typeVarBindings, typePremisses, node.Quan == Quantifier.ALL, diff --git a/Test/test21/BooleanQuantification.bpl b/Test/test21/BooleanQuantification.bpl index 7a0c66d5a..ea5bd6f0b 100644 --- a/Test/test21/BooleanQuantification.bpl +++ b/Test/test21/BooleanQuantification.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -35,4 +33,4 @@ procedure S() returns () { assert (forall x:bool :: g(x) >= 0); assert g((forall x:bool :: g(x) >= 0)) >= 17; assert (forall x:bool :: f(x) == g(x)); // should not be provable -} \ No newline at end of file +} diff --git a/Test/test21/BooleanQuantification.bpl.a.expect b/Test/test21/BooleanQuantification.bpl.a.expect index 4f2f67ff6..2785eee5d 100644 --- a/Test/test21/BooleanQuantification.bpl.a.expect +++ b/Test/test21/BooleanQuantification.bpl.a.expect @@ -1,8 +1,8 @@ -BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold. +BooleanQuantification.bpl(23,3): Error BP5001: This assertion might not hold. Execution trace: - BooleanQuantification.bpl(24,3): anon0 -BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold. + BooleanQuantification.bpl(22,3): anon0 +BooleanQuantification.bpl(35,3): Error BP5001: This assertion might not hold. Execution trace: - BooleanQuantification.bpl(35,3): anon0 + BooleanQuantification.bpl(33,3): anon0 Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/BooleanQuantification.bpl.n.expect b/Test/test21/BooleanQuantification.bpl.n.expect deleted file mode 100644 index 4f2f67ff6..000000000 --- a/Test/test21/BooleanQuantification.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold. -Execution trace: - BooleanQuantification.bpl(24,3): anon0 -BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold. -Execution trace: - BooleanQuantification.bpl(35,3): anon0 - -Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/BooleanQuantification.bpl.p.expect b/Test/test21/BooleanQuantification.bpl.p.expect index 4f2f67ff6..2785eee5d 100644 --- a/Test/test21/BooleanQuantification.bpl.p.expect +++ b/Test/test21/BooleanQuantification.bpl.p.expect @@ -1,8 +1,8 @@ -BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold. +BooleanQuantification.bpl(23,3): Error BP5001: This assertion might not hold. Execution trace: - BooleanQuantification.bpl(24,3): anon0 -BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold. + BooleanQuantification.bpl(22,3): anon0 +BooleanQuantification.bpl(35,3): Error BP5001: This assertion might not hold. Execution trace: - BooleanQuantification.bpl(35,3): anon0 + BooleanQuantification.bpl(33,3): anon0 Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/BooleanQuantification2.bpl b/Test/test21/BooleanQuantification2.bpl index 77ac26c8d..68f7323df 100644 --- a/Test/test21/BooleanQuantification2.bpl +++ b/Test/test21/BooleanQuantification2.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -17,4 +15,4 @@ procedure P() returns () { assert j || !j; assert false; -} \ No newline at end of file +} diff --git a/Test/test21/BooleanQuantification2.bpl.a.expect b/Test/test21/BooleanQuantification2.bpl.a.expect index 8b6378aca..63339b4c6 100644 --- a/Test/test21/BooleanQuantification2.bpl.a.expect +++ b/Test/test21/BooleanQuantification2.bpl.a.expect @@ -1,5 +1,5 @@ -BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold. +BooleanQuantification2.bpl(17,3): Error BP5001: This assertion might not hold. Execution trace: - BooleanQuantification2.bpl(16,3): anon0 + BooleanQuantification2.bpl(14,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/BooleanQuantification2.bpl.n.expect b/Test/test21/BooleanQuantification2.bpl.n.expect deleted file mode 100644 index 8b6378aca..000000000 --- a/Test/test21/BooleanQuantification2.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold. -Execution trace: - BooleanQuantification2.bpl(16,3): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/BooleanQuantification2.bpl.p.expect b/Test/test21/BooleanQuantification2.bpl.p.expect index 8b6378aca..63339b4c6 100644 --- a/Test/test21/BooleanQuantification2.bpl.p.expect +++ b/Test/test21/BooleanQuantification2.bpl.p.expect @@ -1,5 +1,5 @@ -BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold. +BooleanQuantification2.bpl(17,3): Error BP5001: This assertion might not hold. Execution trace: - BooleanQuantification2.bpl(16,3): anon0 + BooleanQuantification2.bpl(14,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Boxing.bpl b/Test/test21/Boxing.bpl index aa7c53b34..39502aefd 100644 --- a/Test/test21/Boxing.bpl +++ b/Test/test21/Boxing.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -24,4 +22,4 @@ procedure P() returns () assert unbox(b1) == 13 && unbox(b2) == true && unbox(unbox(b3)) == 13; assert unbox(b1) == true; // error -} \ No newline at end of file +} diff --git a/Test/test21/Boxing.bpl.a.expect b/Test/test21/Boxing.bpl.a.expect index 092747bc6..8b042d286 100644 --- a/Test/test21/Boxing.bpl.a.expect +++ b/Test/test21/Boxing.bpl.a.expect @@ -1,5 +1,5 @@ -Boxing.bpl(26,3): Error BP5001: This assertion might not hold. +Boxing.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: - Boxing.bpl(21,6): anon0 + Boxing.bpl(19,6): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Boxing.bpl.n.expect b/Test/test21/Boxing.bpl.n.expect deleted file mode 100644 index c19befeec..000000000 --- a/Test/test21/Boxing.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -Boxing.bpl(25,3): Error BP5001: This assertion might not hold. -Execution trace: - Boxing.bpl(21,6): anon0 -Boxing.bpl(26,3): Error BP5001: This assertion might not hold. -Execution trace: - Boxing.bpl(21,6): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Boxing.bpl.p.expect b/Test/test21/Boxing.bpl.p.expect index 092747bc6..8b042d286 100644 --- a/Test/test21/Boxing.bpl.p.expect +++ b/Test/test21/Boxing.bpl.p.expect @@ -1,5 +1,5 @@ -Boxing.bpl(26,3): Error BP5001: This assertion might not hold. +Boxing.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: - Boxing.bpl(21,6): anon0 + Boxing.bpl(19,6): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Casts.bpl b/Test/test21/Casts.bpl index 07494ec1c..9df5a8581 100644 --- a/Test/test21/Casts.bpl +++ b/Test/test21/Casts.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -14,4 +12,4 @@ procedure P() returns () { assert n[m[x]] == 1; assert m[n[x]] == 1; // should not be provable -} \ No newline at end of file +} diff --git a/Test/test21/Casts.bpl.a.expect b/Test/test21/Casts.bpl.a.expect index ecda264e5..48a0d27f1 100644 --- a/Test/test21/Casts.bpl.a.expect +++ b/Test/test21/Casts.bpl.a.expect @@ -1,5 +1,5 @@ -Casts.bpl(16,3): Error BP5001: This assertion might not hold. +Casts.bpl(14,3): Error BP5001: This assertion might not hold. Execution trace: - Casts.bpl(12,3): anon0 + Casts.bpl(10,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Casts.bpl.n.expect b/Test/test21/Casts.bpl.n.expect deleted file mode 100644 index ecda264e5..000000000 --- a/Test/test21/Casts.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -Casts.bpl(16,3): Error BP5001: This assertion might not hold. -Execution trace: - Casts.bpl(12,3): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Casts.bpl.p.expect b/Test/test21/Casts.bpl.p.expect index ecda264e5..48a0d27f1 100644 --- a/Test/test21/Casts.bpl.p.expect +++ b/Test/test21/Casts.bpl.p.expect @@ -1,5 +1,5 @@ -Casts.bpl(16,3): Error BP5001: This assertion might not hold. +Casts.bpl(14,3): Error BP5001: This assertion might not hold. Execution trace: - Casts.bpl(12,3): anon0 + Casts.bpl(10,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Coercions2.bpl b/Test/test21/Coercions2.bpl index a52fb0e65..0644fd6e8 100644 --- a/Test/test21/Coercions2.bpl +++ b/Test/test21/Coercions2.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -27,4 +25,4 @@ procedure P() { assert b == box(i); assert false; -} \ No newline at end of file +} diff --git a/Test/test21/Coercions2.bpl.a.expect b/Test/test21/Coercions2.bpl.a.expect index 04c35bf4e..de7356f4f 100644 --- a/Test/test21/Coercions2.bpl.a.expect +++ b/Test/test21/Coercions2.bpl.a.expect @@ -1,6 +1,6 @@ -Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int -Coercions2.bpl(29,3): Error BP5001: This assertion might not hold. +Coercions2.bpl(16,23): Warning: type parameter a is ambiguous, instantiating to int +Coercions2.bpl(27,3): Error BP5001: This assertion might not hold. Execution trace: - Coercions2.bpl(24,3): anon0 + Coercions2.bpl(22,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Coercions2.bpl.n.expect b/Test/test21/Coercions2.bpl.n.expect deleted file mode 100644 index 121a25ff2..000000000 --- a/Test/test21/Coercions2.bpl.n.expect +++ /dev/null @@ -1,9 +0,0 @@ -Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int -Coercions2.bpl(24,3): Error BP5001: This assertion might not hold. -Execution trace: - Coercions2.bpl(24,3): anon0 -Coercions2.bpl(29,3): Error BP5001: This assertion might not hold. -Execution trace: - Coercions2.bpl(24,3): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Coercions2.bpl.p.expect b/Test/test21/Coercions2.bpl.p.expect index 04c35bf4e..de7356f4f 100644 --- a/Test/test21/Coercions2.bpl.p.expect +++ b/Test/test21/Coercions2.bpl.p.expect @@ -1,6 +1,6 @@ -Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int -Coercions2.bpl(29,3): Error BP5001: This assertion might not hold. +Coercions2.bpl(16,23): Warning: type parameter a is ambiguous, instantiating to int +Coercions2.bpl(27,3): Error BP5001: This assertion might not hold. Execution trace: - Coercions2.bpl(24,3): anon0 + Coercions2.bpl(22,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Colors.bpl b/Test/test21/Colors.bpl index fdfc307ff..625a334a5 100644 --- a/Test/test21/Colors.bpl +++ b/Test/test21/Colors.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -24,4 +22,4 @@ procedure Q() returns () { assume x != Blue && x != Green; assert x == Red; -} \ No newline at end of file +} diff --git a/Test/test21/Colors.bpl.a.expect b/Test/test21/Colors.bpl.a.expect index 4339b7707..5bd264d08 100644 --- a/Test/test21/Colors.bpl.a.expect +++ b/Test/test21/Colors.bpl.a.expect @@ -1,8 +1,8 @@ -Colors.bpl(19,3): Error BP5001: This assertion might not hold. +Colors.bpl(17,3): Error BP5001: This assertion might not hold. Execution trace: - Colors.bpl(18,3): anon0 -Colors.bpl(26,3): Error BP5001: This assertion might not hold. + Colors.bpl(16,3): anon0 +Colors.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: - Colors.bpl(25,3): anon0 + Colors.bpl(23,3): anon0 Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Colors.bpl.n.expect b/Test/test21/Colors.bpl.n.expect deleted file mode 100644 index 4339b7707..000000000 --- a/Test/test21/Colors.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -Colors.bpl(19,3): Error BP5001: This assertion might not hold. -Execution trace: - Colors.bpl(18,3): anon0 -Colors.bpl(26,3): Error BP5001: This assertion might not hold. -Execution trace: - Colors.bpl(25,3): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Colors.bpl.p.expect b/Test/test21/Colors.bpl.p.expect index 4339b7707..5bd264d08 100644 --- a/Test/test21/Colors.bpl.p.expect +++ b/Test/test21/Colors.bpl.p.expect @@ -1,8 +1,8 @@ -Colors.bpl(19,3): Error BP5001: This assertion might not hold. +Colors.bpl(17,3): Error BP5001: This assertion might not hold. Execution trace: - Colors.bpl(18,3): anon0 -Colors.bpl(26,3): Error BP5001: This assertion might not hold. + Colors.bpl(16,3): anon0 +Colors.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: - Colors.bpl(25,3): anon0 + Colors.bpl(23,3): anon0 Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/DisjointDomains.bpl b/Test/test21/DisjointDomains.bpl index 405d325c7..b609582a4 100644 --- a/Test/test21/DisjointDomains.bpl +++ b/Test/test21/DisjointDomains.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/DisjointDomains.bpl.a.expect b/Test/test21/DisjointDomains.bpl.a.expect index e813890c5..8d740dad2 100644 --- a/Test/test21/DisjointDomains.bpl.a.expect +++ b/Test/test21/DisjointDomains.bpl.a.expect @@ -1,11 +1,11 @@ -DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold. +DisjointDomains.bpl(18,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains.bpl(17,3): start -DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold. + DisjointDomains.bpl(15,3): start +DisjointDomains.bpl(25,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains.bpl(26,3): start -DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold. + DisjointDomains.bpl(24,3): start +DisjointDomains.bpl(31,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains.bpl(32,3): start + DisjointDomains.bpl(30,3): start Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/DisjointDomains.bpl.n.expect b/Test/test21/DisjointDomains.bpl.n.expect deleted file mode 100644 index a9949f2e7..000000000 --- a/Test/test21/DisjointDomains.bpl.n.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/test21/DisjointDomains.bpl.p.expect b/Test/test21/DisjointDomains.bpl.p.expect index e813890c5..8d740dad2 100644 --- a/Test/test21/DisjointDomains.bpl.p.expect +++ b/Test/test21/DisjointDomains.bpl.p.expect @@ -1,11 +1,11 @@ -DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold. +DisjointDomains.bpl(18,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains.bpl(17,3): start -DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold. + DisjointDomains.bpl(15,3): start +DisjointDomains.bpl(25,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains.bpl(26,3): start -DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold. + DisjointDomains.bpl(24,3): start +DisjointDomains.bpl(31,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains.bpl(32,3): start + DisjointDomains.bpl(30,3): start Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/DisjointDomains2.bpl b/Test/test21/DisjointDomains2.bpl index 9f9dd63ee..e65544f84 100644 --- a/Test/test21/DisjointDomains2.bpl +++ b/Test/test21/DisjointDomains2.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/DisjointDomains2.bpl.a.expect b/Test/test21/DisjointDomains2.bpl.a.expect index f0f40a57f..6eb1216f7 100644 --- a/Test/test21/DisjointDomains2.bpl.a.expect +++ b/Test/test21/DisjointDomains2.bpl.a.expect @@ -1,20 +1,20 @@ -DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold. +DisjointDomains2.bpl(15,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(15,3): start -DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(13,3): start +DisjointDomains2.bpl(22,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(22,3): start -DisjointDomains2.bpl(38,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(20,3): start +DisjointDomains2.bpl(36,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(36,3): start -DisjointDomains2.bpl(45,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(34,3): start +DisjointDomains2.bpl(43,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(43,3): start -DisjointDomains2.bpl(55,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(41,3): start +DisjointDomains2.bpl(53,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(51,3): start -DisjointDomains2.bpl(69,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(49,3): start +DisjointDomains2.bpl(67,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(64,3): start + DisjointDomains2.bpl(62,3): start Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/test21/DisjointDomains2.bpl.n.expect b/Test/test21/DisjointDomains2.bpl.n.expect deleted file mode 100644 index c378844e5..000000000 --- a/Test/test21/DisjointDomains2.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold. -Execution trace: - DisjointDomains2.bpl(15,3): start -DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold. -Execution trace: - DisjointDomains2.bpl(22,3): start - -Boogie program verifier finished with 4 verified, 2 errors diff --git a/Test/test21/DisjointDomains2.bpl.p.expect b/Test/test21/DisjointDomains2.bpl.p.expect index f0f40a57f..6eb1216f7 100644 --- a/Test/test21/DisjointDomains2.bpl.p.expect +++ b/Test/test21/DisjointDomains2.bpl.p.expect @@ -1,20 +1,20 @@ -DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold. +DisjointDomains2.bpl(15,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(15,3): start -DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(13,3): start +DisjointDomains2.bpl(22,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(22,3): start -DisjointDomains2.bpl(38,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(20,3): start +DisjointDomains2.bpl(36,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(36,3): start -DisjointDomains2.bpl(45,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(34,3): start +DisjointDomains2.bpl(43,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(43,3): start -DisjointDomains2.bpl(55,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(41,3): start +DisjointDomains2.bpl(53,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(51,3): start -DisjointDomains2.bpl(69,5): Error BP5001: This assertion might not hold. + DisjointDomains2.bpl(49,3): start +DisjointDomains2.bpl(67,5): Error BP5001: This assertion might not hold. Execution trace: - DisjointDomains2.bpl(64,3): start + DisjointDomains2.bpl(62,3): start Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/test21/EmptyList.bpl b/Test/test21/EmptyList.bpl index 6acd2736e..0bcec5cd8 100644 --- a/Test/test21/EmptyList.bpl +++ b/Test/test21/EmptyList.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -50,4 +48,4 @@ procedure P() returns () procedure Q() returns () { assert Cons(NIL(), NIL()) != NIL(); // warning, but provable -} \ No newline at end of file +} diff --git a/Test/test21/EmptyList.bpl.a.expect b/Test/test21/EmptyList.bpl.a.expect index c15d8d6f4..a072a5e54 100644 --- a/Test/test21/EmptyList.bpl.a.expect +++ b/Test/test21/EmptyList.bpl.a.expect @@ -1,6 +1,6 @@ -EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int -EmptyList.bpl(48,3): Error BP5001: This assertion might not hold. +EmptyList.bpl(50,9): Warning: type parameter a is ambiguous, instantiating to List int +EmptyList.bpl(46,3): Error BP5001: This assertion might not hold. Execution trace: - EmptyList.bpl(32,5): anon0 + EmptyList.bpl(30,5): anon0 Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/EmptyList.bpl.n.expect b/Test/test21/EmptyList.bpl.n.expect deleted file mode 100644 index 3895affe8..000000000 --- a/Test/test21/EmptyList.bpl.n.expect +++ /dev/null @@ -1,12 +0,0 @@ -EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int -EmptyList.bpl(34,3): Error BP5001: This assertion might not hold. -Execution trace: - EmptyList.bpl(32,5): anon0 -EmptyList.bpl(48,3): Error BP5001: This assertion might not hold. -Execution trace: - EmptyList.bpl(32,5): anon0 -EmptyList.bpl(52,3): Error BP5001: This assertion might not hold. -Execution trace: - EmptyList.bpl(52,3): anon0 - -Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/EmptyList.bpl.p.expect b/Test/test21/EmptyList.bpl.p.expect index c15d8d6f4..a072a5e54 100644 --- a/Test/test21/EmptyList.bpl.p.expect +++ b/Test/test21/EmptyList.bpl.p.expect @@ -1,6 +1,6 @@ -EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int -EmptyList.bpl(48,3): Error BP5001: This assertion might not hold. +EmptyList.bpl(50,9): Warning: type parameter a is ambiguous, instantiating to List int +EmptyList.bpl(46,3): Error BP5001: This assertion might not hold. Execution trace: - EmptyList.bpl(32,5): anon0 + EmptyList.bpl(30,5): anon0 Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/EmptySetBug.bpl b/Test/test21/EmptySetBug.bpl index 6c25ed95b..afd9cdf27 100644 --- a/Test/test21/EmptySetBug.bpl +++ b/Test/test21/EmptySetBug.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/EmptySetBug.bpl.a.expect b/Test/test21/EmptySetBug.bpl.a.expect index 8b3d17b8c..e3d4e6451 100644 --- a/Test/test21/EmptySetBug.bpl.a.expect +++ b/Test/test21/EmptySetBug.bpl.a.expect @@ -1,5 +1,5 @@ -EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold. +EmptySetBug.bpl(33,3): Error BP5001: This assertion might not hold. Execution trace: - EmptySetBug.bpl(31,5): anon0 + EmptySetBug.bpl(29,5): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/EmptySetBug.bpl.n.expect b/Test/test21/EmptySetBug.bpl.n.expect deleted file mode 100644 index a37a8c141..000000000 --- a/Test/test21/EmptySetBug.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -EmptySetBug.bpl(33,3): Error BP5001: This assertion might not hold. -Execution trace: - EmptySetBug.bpl(31,5): anon0 -EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold. -Execution trace: - EmptySetBug.bpl(31,5): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/EmptySetBug.bpl.p.expect b/Test/test21/EmptySetBug.bpl.p.expect index 8b3d17b8c..e3d4e6451 100644 --- a/Test/test21/EmptySetBug.bpl.p.expect +++ b/Test/test21/EmptySetBug.bpl.p.expect @@ -1,5 +1,5 @@ -EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold. +EmptySetBug.bpl(33,3): Error BP5001: This assertion might not hold. Execution trace: - EmptySetBug.bpl(31,5): anon0 + EmptySetBug.bpl(29,5): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Flattening.bpl b/Test/test21/Flattening.bpl index 3931c573d..8f7ed7d0f 100644 --- a/Test/test21/Flattening.bpl +++ b/Test/test21/Flattening.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -16,4 +14,4 @@ axiom (f((exists x:int :: g(f((forall y:int :: g(x+y) >= 0))) >= 12)) == 3); procedure P() returns () { assert false; -} \ No newline at end of file +} diff --git a/Test/test21/Flattening.bpl.a.expect b/Test/test21/Flattening.bpl.a.expect index e68a8891e..56bad3291 100644 --- a/Test/test21/Flattening.bpl.a.expect +++ b/Test/test21/Flattening.bpl.a.expect @@ -1,5 +1,5 @@ -Flattening.bpl(18,3): Error BP5001: This assertion might not hold. +Flattening.bpl(16,3): Error BP5001: This assertion might not hold. Execution trace: - Flattening.bpl(18,3): anon0 + Flattening.bpl(16,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Flattening.bpl.n.expect b/Test/test21/Flattening.bpl.n.expect deleted file mode 100644 index e68a8891e..000000000 --- a/Test/test21/Flattening.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -Flattening.bpl(18,3): Error BP5001: This assertion might not hold. -Execution trace: - Flattening.bpl(18,3): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Flattening.bpl.p.expect b/Test/test21/Flattening.bpl.p.expect index e68a8891e..56bad3291 100644 --- a/Test/test21/Flattening.bpl.p.expect +++ b/Test/test21/Flattening.bpl.p.expect @@ -1,5 +1,5 @@ -Flattening.bpl(18,3): Error BP5001: This assertion might not hold. +Flattening.bpl(16,3): Error BP5001: This assertion might not hold. Execution trace: - Flattening.bpl(18,3): anon0 + Flattening.bpl(16,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/FunAxioms.bpl b/Test/test21/FunAxioms.bpl index 2baa2169d..6b0555bb7 100644 --- a/Test/test21/FunAxioms.bpl +++ b/Test/test21/FunAxioms.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -43,4 +41,4 @@ procedure Q() returns () { assert Right(MP(1,3)) == 3; assert Right(MP(1,true)) == true; -} \ No newline at end of file +} diff --git a/Test/test21/FunAxioms.bpl.a.expect b/Test/test21/FunAxioms.bpl.a.expect index b6fa4917e..858214c52 100644 --- a/Test/test21/FunAxioms.bpl.a.expect +++ b/Test/test21/FunAxioms.bpl.a.expect @@ -1,5 +1,5 @@ -FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold. +FunAxioms.bpl(34,3): Error BP5001: This assertion might not hold. Execution trace: - FunAxioms.bpl(24,3): anon0 + FunAxioms.bpl(22,3): anon0 Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/FunAxioms.bpl.n.expect b/Test/test21/FunAxioms.bpl.n.expect deleted file mode 100644 index b6fa4917e..000000000 --- a/Test/test21/FunAxioms.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold. -Execution trace: - FunAxioms.bpl(24,3): anon0 - -Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/FunAxioms.bpl.p.expect b/Test/test21/FunAxioms.bpl.p.expect index b6fa4917e..858214c52 100644 --- a/Test/test21/FunAxioms.bpl.p.expect +++ b/Test/test21/FunAxioms.bpl.p.expect @@ -1,5 +1,5 @@ -FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold. +FunAxioms.bpl(34,3): Error BP5001: This assertion might not hold. Execution trace: - FunAxioms.bpl(24,3): anon0 + FunAxioms.bpl(22,3): anon0 Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/FunAxioms2.bpl b/Test/test21/FunAxioms2.bpl index 341807f82..2c66ffc8a 100644 --- a/Test/test21/FunAxioms2.bpl +++ b/Test/test21/FunAxioms2.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -24,4 +22,4 @@ procedure P() returns () { assert x >= 0 && f() >= 7; assert g() != c; assert f() >= 20; // should not be provable -} \ No newline at end of file +} diff --git a/Test/test21/FunAxioms2.bpl.a.expect b/Test/test21/FunAxioms2.bpl.a.expect index bf34a7a05..03b15fec9 100644 --- a/Test/test21/FunAxioms2.bpl.a.expect +++ b/Test/test21/FunAxioms2.bpl.a.expect @@ -1,5 +1,5 @@ -FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold. +FunAxioms2.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: - FunAxioms2.bpl(22,5): anon0 + FunAxioms2.bpl(20,5): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/FunAxioms2.bpl.n.expect b/Test/test21/FunAxioms2.bpl.n.expect deleted file mode 100644 index bf34a7a05..000000000 --- a/Test/test21/FunAxioms2.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold. -Execution trace: - FunAxioms2.bpl(22,5): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/FunAxioms2.bpl.p.expect b/Test/test21/FunAxioms2.bpl.p.expect index bf34a7a05..03b15fec9 100644 --- a/Test/test21/FunAxioms2.bpl.p.expect +++ b/Test/test21/FunAxioms2.bpl.p.expect @@ -1,5 +1,5 @@ -FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold. +FunAxioms2.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: - FunAxioms2.bpl(22,5): anon0 + FunAxioms2.bpl(20,5): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAbstraction.bpl b/Test/test21/HeapAbstraction.bpl index b1abf0c06..8310ee042 100644 --- a/Test/test21/HeapAbstraction.bpl +++ b/Test/test21/HeapAbstraction.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/HeapAbstraction.bpl.a.expect b/Test/test21/HeapAbstraction.bpl.a.expect index 1058ef91f..8fb246c25 100644 --- a/Test/test21/HeapAbstraction.bpl.a.expect +++ b/Test/test21/HeapAbstraction.bpl.a.expect @@ -1,5 +1,5 @@ -HeapAbstraction.bpl(21,3): Error BP5001: This assertion might not hold. +HeapAbstraction.bpl(19,3): Error BP5001: This assertion might not hold. Execution trace: - HeapAbstraction.bpl(20,3): anon0 + HeapAbstraction.bpl(18,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAbstraction.bpl.n.expect b/Test/test21/HeapAbstraction.bpl.n.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/test21/HeapAbstraction.bpl.n.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/HeapAbstraction.bpl.p.expect b/Test/test21/HeapAbstraction.bpl.p.expect index 1058ef91f..8fb246c25 100644 --- a/Test/test21/HeapAbstraction.bpl.p.expect +++ b/Test/test21/HeapAbstraction.bpl.p.expect @@ -1,5 +1,5 @@ -HeapAbstraction.bpl(21,3): Error BP5001: This assertion might not hold. +HeapAbstraction.bpl(19,3): Error BP5001: This assertion might not hold. Execution trace: - HeapAbstraction.bpl(20,3): anon0 + HeapAbstraction.bpl(18,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAxiom.bpl b/Test/test21/HeapAxiom.bpl index a49ddd367..f5e0c5987 100644 --- a/Test/test21/HeapAxiom.bpl +++ b/Test/test21/HeapAxiom.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/HeapAxiom.bpl.a.expect b/Test/test21/HeapAxiom.bpl.a.expect index 26a961054..2b0f7882f 100644 --- a/Test/test21/HeapAxiom.bpl.a.expect +++ b/Test/test21/HeapAxiom.bpl.a.expect @@ -1,5 +1,5 @@ -HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold. +HeapAxiom.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - HeapAxiom.bpl(19,3): anon0 + HeapAxiom.bpl(17,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAxiom.bpl.n.expect b/Test/test21/HeapAxiom.bpl.n.expect deleted file mode 100644 index 26a961054..000000000 --- a/Test/test21/HeapAxiom.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold. -Execution trace: - HeapAxiom.bpl(19,3): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAxiom.bpl.p.expect b/Test/test21/HeapAxiom.bpl.p.expect index 26a961054..2b0f7882f 100644 --- a/Test/test21/HeapAxiom.bpl.p.expect +++ b/Test/test21/HeapAxiom.bpl.p.expect @@ -1,5 +1,5 @@ -HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold. +HeapAxiom.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - HeapAxiom.bpl(19,3): anon0 + HeapAxiom.bpl(17,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples0.bpl b/Test/test21/InterestingExamples0.bpl index fd79ad5c9..8a29aa577 100644 --- a/Test/test21/InterestingExamples0.bpl +++ b/Test/test21/InterestingExamples0.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -11,4 +9,4 @@ var a : [t]int; a[5] := 0; a[true] := 1; assert a[5] == 0; -} \ No newline at end of file +} diff --git a/Test/test21/InterestingExamples0.bpl.n.expect b/Test/test21/InterestingExamples0.bpl.n.expect deleted file mode 100644 index f549a09a9..000000000 --- a/Test/test21/InterestingExamples0.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -InterestingExamples0.bpl(13,1): Error BP5001: This assertion might not hold. -Execution trace: - InterestingExamples0.bpl(11,6): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples1.bpl b/Test/test21/InterestingExamples1.bpl index 48b4a5dd2..fd02e6a2c 100644 --- a/Test/test21/InterestingExamples1.bpl +++ b/Test/test21/InterestingExamples1.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/InterestingExamples1.bpl.a.expect b/Test/test21/InterestingExamples1.bpl.a.expect index 8ee75548a..935886799 100644 --- a/Test/test21/InterestingExamples1.bpl.a.expect +++ b/Test/test21/InterestingExamples1.bpl.a.expect @@ -1,5 +1,5 @@ -InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold. +InterestingExamples1.bpl(26,3): Error BP5001: This assertion might not hold. Execution trace: - InterestingExamples1.bpl(19,5): anon0 + InterestingExamples1.bpl(17,5): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples1.bpl.n.expect b/Test/test21/InterestingExamples1.bpl.n.expect deleted file mode 100644 index b757672bc..000000000 --- a/Test/test21/InterestingExamples1.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold. -Execution trace: - InterestingExamples1.bpl(19,5): anon0 -InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold. -Execution trace: - InterestingExamples1.bpl(19,5): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/InterestingExamples1.bpl.p.expect b/Test/test21/InterestingExamples1.bpl.p.expect index 8ee75548a..935886799 100644 --- a/Test/test21/InterestingExamples1.bpl.p.expect +++ b/Test/test21/InterestingExamples1.bpl.p.expect @@ -1,5 +1,5 @@ -InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold. +InterestingExamples1.bpl(26,3): Error BP5001: This assertion might not hold. Execution trace: - InterestingExamples1.bpl(19,5): anon0 + InterestingExamples1.bpl(17,5): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples2.bpl b/Test/test21/InterestingExamples2.bpl index 4c07ee686..50e2f7ad6 100644 --- a/Test/test21/InterestingExamples2.bpl +++ b/Test/test21/InterestingExamples2.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/InterestingExamples2.bpl.n.expect b/Test/test21/InterestingExamples2.bpl.n.expect deleted file mode 100644 index 389abe514..000000000 --- a/Test/test21/InterestingExamples2.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -InterestingExamples2.bpl(15,1): Error BP5001: This assertion might not hold. -Execution trace: - InterestingExamples2.bpl(14,6): anon0 -InterestingExamples2.bpl(16,1): Error BP5001: This assertion might not hold. -Execution trace: - InterestingExamples2.bpl(14,6): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/InterestingExamples3.bpl b/Test/test21/InterestingExamples3.bpl index 4990fb729..1698cf67d 100644 --- a/Test/test21/InterestingExamples3.bpl +++ b/Test/test21/InterestingExamples3.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/InterestingExamples3.bpl.a.expect b/Test/test21/InterestingExamples3.bpl.a.expect index b02bbbdfd..0a09edcc7 100644 --- a/Test/test21/InterestingExamples3.bpl.a.expect +++ b/Test/test21/InterestingExamples3.bpl.a.expect @@ -1,5 +1,5 @@ -InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold. +InterestingExamples3.bpl(19,2): Error BP5001: This assertion might not hold. Execution trace: - InterestingExamples3.bpl(19,2): anon0 + InterestingExamples3.bpl(17,2): anon0 Boogie program verifier finished with 2 verified, 1 error diff --git a/Test/test21/InterestingExamples3.bpl.n.expect b/Test/test21/InterestingExamples3.bpl.n.expect deleted file mode 100644 index b02bbbdfd..000000000 --- a/Test/test21/InterestingExamples3.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold. -Execution trace: - InterestingExamples3.bpl(19,2): anon0 - -Boogie program verifier finished with 2 verified, 1 error diff --git a/Test/test21/InterestingExamples3.bpl.p.expect b/Test/test21/InterestingExamples3.bpl.p.expect index b02bbbdfd..0a09edcc7 100644 --- a/Test/test21/InterestingExamples3.bpl.p.expect +++ b/Test/test21/InterestingExamples3.bpl.p.expect @@ -1,5 +1,5 @@ -InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold. +InterestingExamples3.bpl(19,2): Error BP5001: This assertion might not hold. Execution trace: - InterestingExamples3.bpl(19,2): anon0 + InterestingExamples3.bpl(17,2): anon0 Boogie program verifier finished with 2 verified, 1 error diff --git a/Test/test21/InterestingExamples4.bpl b/Test/test21/InterestingExamples4.bpl index aa8993db7..b36858216 100644 --- a/Test/test21/InterestingExamples4.bpl +++ b/Test/test21/InterestingExamples4.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/InterestingExamples4.bpl.a.expect b/Test/test21/InterestingExamples4.bpl.a.expect index 346e844b4..af141bf97 100644 --- a/Test/test21/InterestingExamples4.bpl.a.expect +++ b/Test/test21/InterestingExamples4.bpl.a.expect @@ -1,8 +1,8 @@ -InterestingExamples4.bpl(42,3): Error BP5001: This assertion might not hold. +InterestingExamples4.bpl(40,3): Error BP5001: This assertion might not hold. Execution trace: - InterestingExamples4.bpl(42,3): anon0 -InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold. + InterestingExamples4.bpl(40,3): anon0 +InterestingExamples4.bpl(43,3): Error BP5001: This assertion might not hold. Execution trace: - InterestingExamples4.bpl(42,3): anon0 + InterestingExamples4.bpl(40,3): anon0 Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/InterestingExamples4.bpl.n.expect b/Test/test21/InterestingExamples4.bpl.n.expect deleted file mode 100644 index 346e844b4..000000000 --- a/Test/test21/InterestingExamples4.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -InterestingExamples4.bpl(42,3): Error BP5001: This assertion might not hold. -Execution trace: - InterestingExamples4.bpl(42,3): anon0 -InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold. -Execution trace: - InterestingExamples4.bpl(42,3): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/InterestingExamples4.bpl.p.expect b/Test/test21/InterestingExamples4.bpl.p.expect index bb912e592..9f2d0993c 100644 --- a/Test/test21/InterestingExamples4.bpl.p.expect +++ b/Test/test21/InterestingExamples4.bpl.p.expect @@ -1,5 +1,5 @@ -InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold. +InterestingExamples4.bpl(43,3): Error BP5001: This assertion might not hold. Execution trace: - InterestingExamples4.bpl(42,3): anon0 + InterestingExamples4.bpl(40,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples5.bpl b/Test/test21/InterestingExamples5.bpl index 8eadadc9c..8231b7290 100644 --- a/Test/test21/InterestingExamples5.bpl +++ b/Test/test21/InterestingExamples5.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -19,4 +17,4 @@ procedure P() returns () { var z : C int; assume g(z) == z; assert (exists x : C int :: f(x) == 42); -} \ No newline at end of file +} diff --git a/Test/test21/InterestingExamples5.bpl.n.expect b/Test/test21/InterestingExamples5.bpl.n.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/test21/InterestingExamples5.bpl.n.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Keywords.bpl b/Test/test21/Keywords.bpl index 53a323cd5..c08136684 100644 --- a/Test/test21/Keywords.bpl +++ b/Test/test21/Keywords.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -12,4 +10,4 @@ axiom (forall x:int :: NOT(x) == 1 - x); procedure P() returns () { assert NOT(5) == -4; -} \ No newline at end of file +} diff --git a/Test/test21/Keywords.bpl.n.expect b/Test/test21/Keywords.bpl.n.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/test21/Keywords.bpl.n.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/LargeLiterals0.bpl b/Test/test21/LargeLiterals0.bpl index 0f6029107..5563bb45f 100644 --- a/Test/test21/LargeLiterals0.bpl +++ b/Test/test21/LargeLiterals0.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -23,4 +21,4 @@ procedure P() modifies x; { assert x < -123456789; // error -} \ No newline at end of file +} diff --git a/Test/test21/LargeLiterals0.bpl.a.expect b/Test/test21/LargeLiterals0.bpl.a.expect index 1f42b69e2..72cc2cf24 100644 --- a/Test/test21/LargeLiterals0.bpl.a.expect +++ b/Test/test21/LargeLiterals0.bpl.a.expect @@ -1,5 +1,5 @@ -LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold. +LargeLiterals0.bpl(22,3): Error BP5001: This assertion might not hold. Execution trace: - LargeLiterals0.bpl(13,5): anon0 + LargeLiterals0.bpl(11,5): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/LargeLiterals0.bpl.n.expect b/Test/test21/LargeLiterals0.bpl.n.expect deleted file mode 100644 index 1f42b69e2..000000000 --- a/Test/test21/LargeLiterals0.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold. -Execution trace: - LargeLiterals0.bpl(13,5): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/LargeLiterals0.bpl.p.expect b/Test/test21/LargeLiterals0.bpl.p.expect index 1f42b69e2..72cc2cf24 100644 --- a/Test/test21/LargeLiterals0.bpl.p.expect +++ b/Test/test21/LargeLiterals0.bpl.p.expect @@ -1,5 +1,5 @@ -LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold. +LargeLiterals0.bpl(22,3): Error BP5001: This assertion might not hold. Execution trace: - LargeLiterals0.bpl(13,5): anon0 + LargeLiterals0.bpl(11,5): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/LetSorting.bpl b/Test/test21/LetSorting.bpl index 9c76dbea8..79d21765b 100644 --- a/Test/test21/LetSorting.bpl +++ b/Test/test21/LetSorting.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/LetSorting.bpl.n.expect b/Test/test21/LetSorting.bpl.n.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/test21/LetSorting.bpl.n.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl index 4020c00da..222b60e0a 100644 --- a/Test/test21/MapAxiomsConsistency.bpl +++ b/Test/test21/MapAxiomsConsistency.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/MapAxiomsConsistency.bpl.a.expect b/Test/test21/MapAxiomsConsistency.bpl.a.expect index eabc661f4..c7e173466 100644 --- a/Test/test21/MapAxiomsConsistency.bpl.a.expect +++ b/Test/test21/MapAxiomsConsistency.bpl.a.expect @@ -1,5 +1,5 @@ -MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold. +MapAxiomsConsistency.bpl(98,5): Error BP5001: This assertion might not hold. Execution trace: - MapAxiomsConsistency.bpl(85,13): anon0 + MapAxiomsConsistency.bpl(83,13): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/MapAxiomsConsistency.bpl.n.expect b/Test/test21/MapAxiomsConsistency.bpl.n.expect deleted file mode 100644 index eabc661f4..000000000 --- a/Test/test21/MapAxiomsConsistency.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold. -Execution trace: - MapAxiomsConsistency.bpl(85,13): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/MapAxiomsConsistency.bpl.p.expect b/Test/test21/MapAxiomsConsistency.bpl.p.expect index eabc661f4..c7e173466 100644 --- a/Test/test21/MapAxiomsConsistency.bpl.p.expect +++ b/Test/test21/MapAxiomsConsistency.bpl.p.expect @@ -1,5 +1,5 @@ -MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold. +MapAxiomsConsistency.bpl(98,5): Error BP5001: This assertion might not hold. Execution trace: - MapAxiomsConsistency.bpl(85,13): anon0 + MapAxiomsConsistency.bpl(83,13): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/MapOutputTypeParams.bpl b/Test/test21/MapOutputTypeParams.bpl index 484c7dc19..d027273f2 100644 --- a/Test/test21/MapOutputTypeParams.bpl +++ b/Test/test21/MapOutputTypeParams.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -36,4 +34,4 @@ procedure R() returns () modifies p; { assert p[7] == 28; assert p[6] == 28; // error -} \ No newline at end of file +} diff --git a/Test/test21/MapOutputTypeParams.bpl.a.expect b/Test/test21/MapOutputTypeParams.bpl.a.expect index 5e4aa0be8..990af1ce3 100644 --- a/Test/test21/MapOutputTypeParams.bpl.a.expect +++ b/Test/test21/MapOutputTypeParams.bpl.a.expect @@ -1,12 +1,12 @@ -MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int -MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold. +MapOutputTypeParams.bpl(33,3): Warning: type parameter a is ambiguous, instantiating to int +MapOutputTypeParams.bpl(17,3): Error BP5001: This assertion might not hold. Execution trace: - MapOutputTypeParams.bpl(13,9): anon0 -MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold. + MapOutputTypeParams.bpl(11,9): anon0 +MapOutputTypeParams.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - MapOutputTypeParams.bpl(25,9): anon0 -MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold. + MapOutputTypeParams.bpl(23,9): anon0 +MapOutputTypeParams.bpl(36,3): Error BP5001: This assertion might not hold. Execution trace: - MapOutputTypeParams.bpl(34,8): anon0 + MapOutputTypeParams.bpl(32,8): anon0 Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/MapOutputTypeParams.bpl.n.expect b/Test/test21/MapOutputTypeParams.bpl.n.expect deleted file mode 100644 index 3c56324d8..000000000 --- a/Test/test21/MapOutputTypeParams.bpl.n.expect +++ /dev/null @@ -1,21 +0,0 @@ -MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int -MapOutputTypeParams.bpl(18,3): Error BP5001: This assertion might not hold. -Execution trace: - MapOutputTypeParams.bpl(13,9): anon0 -MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold. -Execution trace: - MapOutputTypeParams.bpl(13,9): anon0 -MapOutputTypeParams.bpl(29,3): Error BP5001: This assertion might not hold. -Execution trace: - MapOutputTypeParams.bpl(25,9): anon0 -MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold. -Execution trace: - MapOutputTypeParams.bpl(25,9): anon0 -MapOutputTypeParams.bpl(37,3): Error BP5001: This assertion might not hold. -Execution trace: - MapOutputTypeParams.bpl(34,8): anon0 -MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold. -Execution trace: - MapOutputTypeParams.bpl(34,8): anon0 - -Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/test21/MapOutputTypeParams.bpl.p.expect b/Test/test21/MapOutputTypeParams.bpl.p.expect index 5e4aa0be8..990af1ce3 100644 --- a/Test/test21/MapOutputTypeParams.bpl.p.expect +++ b/Test/test21/MapOutputTypeParams.bpl.p.expect @@ -1,12 +1,12 @@ -MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int -MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold. +MapOutputTypeParams.bpl(33,3): Warning: type parameter a is ambiguous, instantiating to int +MapOutputTypeParams.bpl(17,3): Error BP5001: This assertion might not hold. Execution trace: - MapOutputTypeParams.bpl(13,9): anon0 -MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold. + MapOutputTypeParams.bpl(11,9): anon0 +MapOutputTypeParams.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - MapOutputTypeParams.bpl(25,9): anon0 -MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold. + MapOutputTypeParams.bpl(23,9): anon0 +MapOutputTypeParams.bpl(36,3): Error BP5001: This assertion might not hold. Execution trace: - MapOutputTypeParams.bpl(34,8): anon0 + MapOutputTypeParams.bpl(32,8): anon0 Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Maps0.bpl b/Test/test21/Maps0.bpl index f64bd336c..f43888c3d 100644 --- a/Test/test21/Maps0.bpl +++ b/Test/test21/Maps0.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -43,7 +41,7 @@ procedure R() returns () { var o : ref; var e : Field int, g : Field bool, h : Field (Field int), i : Field int; var heap2 : [ref, Field a] a; - + heap2 := heap; heap2[o, e] := 17; assert heap2 == heap[o, e := 17]; diff --git a/Test/test21/Maps0.bpl.a.expect b/Test/test21/Maps0.bpl.a.expect index ff15a125b..3775df4e7 100644 --- a/Test/test21/Maps0.bpl.a.expect +++ b/Test/test21/Maps0.bpl.a.expect @@ -1,11 +1,11 @@ -Maps0.bpl(29,3): Error BP5001: This assertion might not hold. +Maps0.bpl(27,3): Error BP5001: This assertion might not hold. Execution trace: - Maps0.bpl(20,3): anon0 -Maps0.bpl(38,3): Error BP5001: This assertion might not hold. + Maps0.bpl(18,3): anon0 +Maps0.bpl(36,3): Error BP5001: This assertion might not hold. Execution trace: - Maps0.bpl(38,3): anon0 -Maps0.bpl(59,3): Error BP5001: This assertion might not hold. + Maps0.bpl(36,3): anon0 +Maps0.bpl(57,3): Error BP5001: This assertion might not hold. Execution trace: - Maps0.bpl(47,9): anon0 + Maps0.bpl(45,9): anon0 Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Maps0.bpl.n.expect b/Test/test21/Maps0.bpl.n.expect deleted file mode 100644 index 4ca5c450c..000000000 --- a/Test/test21/Maps0.bpl.n.expect +++ /dev/null @@ -1,17 +0,0 @@ -Maps0.bpl(29,3): Error BP5001: This assertion might not hold. -Execution trace: - Maps0.bpl(20,3): anon0 -Maps0.bpl(52,3): Error BP5001: This assertion might not hold. -Execution trace: - Maps0.bpl(47,9): anon0 -Maps0.bpl(55,3): Error BP5001: This assertion might not hold. -Execution trace: - Maps0.bpl(47,9): anon0 -Maps0.bpl(58,3): Error BP5001: This assertion might not hold. -Execution trace: - Maps0.bpl(47,9): anon0 -Maps0.bpl(59,3): Error BP5001: This assertion might not hold. -Execution trace: - Maps0.bpl(47,9): anon0 - -Boogie program verifier finished with 1 verified, 5 errors diff --git a/Test/test21/Maps0.bpl.p.expect b/Test/test21/Maps0.bpl.p.expect index ff15a125b..3775df4e7 100644 --- a/Test/test21/Maps0.bpl.p.expect +++ b/Test/test21/Maps0.bpl.p.expect @@ -1,11 +1,11 @@ -Maps0.bpl(29,3): Error BP5001: This assertion might not hold. +Maps0.bpl(27,3): Error BP5001: This assertion might not hold. Execution trace: - Maps0.bpl(20,3): anon0 -Maps0.bpl(38,3): Error BP5001: This assertion might not hold. + Maps0.bpl(18,3): anon0 +Maps0.bpl(36,3): Error BP5001: This assertion might not hold. Execution trace: - Maps0.bpl(38,3): anon0 -Maps0.bpl(59,3): Error BP5001: This assertion might not hold. + Maps0.bpl(36,3): anon0 +Maps0.bpl(57,3): Error BP5001: This assertion might not hold. Execution trace: - Maps0.bpl(47,9): anon0 + Maps0.bpl(45,9): anon0 Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Maps1.bpl b/Test/test21/Maps1.bpl index bcb5a9b9f..09cab388c 100644 --- a/Test/test21/Maps1.bpl +++ b/Test/test21/Maps1.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/Maps1.bpl.a.expect b/Test/test21/Maps1.bpl.a.expect index 230f04b8d..120dfa01a 100644 --- a/Test/test21/Maps1.bpl.a.expect +++ b/Test/test21/Maps1.bpl.a.expect @@ -1,5 +1,5 @@ -Maps1.bpl(37,3): Error BP5001: This assertion might not hold. +Maps1.bpl(35,3): Error BP5001: This assertion might not hold. Execution trace: - Maps1.bpl(25,3): anon0 + Maps1.bpl(23,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Maps1.bpl.n.expect b/Test/test21/Maps1.bpl.n.expect deleted file mode 100644 index 48be36cc8..000000000 --- a/Test/test21/Maps1.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -Maps1.bpl(32,3): Error BP5001: This assertion might not hold. -Execution trace: - Maps1.bpl(25,3): anon0 -Maps1.bpl(37,3): Error BP5001: This assertion might not hold. -Execution trace: - Maps1.bpl(25,3): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Maps1.bpl.p.expect b/Test/test21/Maps1.bpl.p.expect index 230f04b8d..120dfa01a 100644 --- a/Test/test21/Maps1.bpl.p.expect +++ b/Test/test21/Maps1.bpl.p.expect @@ -1,5 +1,5 @@ -Maps1.bpl(37,3): Error BP5001: This assertion might not hold. +Maps1.bpl(35,3): Error BP5001: This assertion might not hold. Execution trace: - Maps1.bpl(25,3): anon0 + Maps1.bpl(23,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Maps2.bpl b/Test/test21/Maps2.bpl index 9713875f5..bfea4e8e8 100644 --- a/Test/test21/Maps2.bpl +++ b/Test/test21/Maps2.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" diff --git a/Test/test21/NameClash.bpl b/Test/test21/NameClash.bpl index 59f361a87..477b9faea 100644 --- a/Test/test21/NameClash.bpl +++ b/Test/test21/NameClash.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -11,4 +9,4 @@ axiom f(13) == 0; procedure P() returns () { assert (exists f:int :: 0 == f(f)); -} \ No newline at end of file +} diff --git a/Test/test21/NameClash.bpl.n.expect b/Test/test21/NameClash.bpl.n.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/test21/NameClash.bpl.n.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Orderings.bpl b/Test/test21/Orderings.bpl index 158f0e890..4a6f2ef38 100644 --- a/Test/test21/Orderings.bpl +++ b/Test/test21/Orderings.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -23,4 +21,4 @@ procedure P() returns () { procedure Q() returns () { assume b <: a; assert b == a; -} \ No newline at end of file +} diff --git a/Test/test21/Orderings.bpl.a.expect b/Test/test21/Orderings.bpl.a.expect index a603901c4..83ec50a25 100644 --- a/Test/test21/Orderings.bpl.a.expect +++ b/Test/test21/Orderings.bpl.a.expect @@ -1,5 +1,5 @@ -Orderings.bpl(20,3): Error BP5001: This assertion might not hold. +Orderings.bpl(18,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings.bpl(15,3): anon0 + Orderings.bpl(13,3): anon0 Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/Orderings.bpl.n.expect b/Test/test21/Orderings.bpl.n.expect deleted file mode 100644 index a603901c4..000000000 --- a/Test/test21/Orderings.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -Orderings.bpl(20,3): Error BP5001: This assertion might not hold. -Execution trace: - Orderings.bpl(15,3): anon0 - -Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/Orderings.bpl.p.expect b/Test/test21/Orderings.bpl.p.expect index a603901c4..83ec50a25 100644 --- a/Test/test21/Orderings.bpl.p.expect +++ b/Test/test21/Orderings.bpl.p.expect @@ -1,5 +1,5 @@ -Orderings.bpl(20,3): Error BP5001: This assertion might not hold. +Orderings.bpl(18,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings.bpl(15,3): anon0 + Orderings.bpl(13,3): anon0 Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/Orderings2.bpl b/Test/test21/Orderings2.bpl index c475ca79d..a6f3f3f3d 100644 --- a/Test/test21/Orderings2.bpl +++ b/Test/test21/Orderings2.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -21,4 +19,4 @@ procedure P() returns () { assert x <: d; assert b <: x; // should not be provable -} \ No newline at end of file +} diff --git a/Test/test21/Orderings2.bpl.a.expect b/Test/test21/Orderings2.bpl.a.expect index c949b4d53..fff6f7792 100644 --- a/Test/test21/Orderings2.bpl.a.expect +++ b/Test/test21/Orderings2.bpl.a.expect @@ -1,5 +1,5 @@ -Orderings2.bpl(23,3): Error BP5001: This assertion might not hold. +Orderings2.bpl(21,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings2.bpl(18,3): anon0 + Orderings2.bpl(16,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings2.bpl.n.expect b/Test/test21/Orderings2.bpl.n.expect deleted file mode 100644 index c949b4d53..000000000 --- a/Test/test21/Orderings2.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -Orderings2.bpl(23,3): Error BP5001: This assertion might not hold. -Execution trace: - Orderings2.bpl(18,3): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings2.bpl.p.expect b/Test/test21/Orderings2.bpl.p.expect index c949b4d53..fff6f7792 100644 --- a/Test/test21/Orderings2.bpl.p.expect +++ b/Test/test21/Orderings2.bpl.p.expect @@ -1,5 +1,5 @@ -Orderings2.bpl(23,3): Error BP5001: This assertion might not hold. +Orderings2.bpl(21,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings2.bpl(18,3): anon0 + Orderings2.bpl(16,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings3.bpl b/Test/test21/Orderings3.bpl index 82b619ac5..7f378da2d 100644 --- a/Test/test21/Orderings3.bpl +++ b/Test/test21/Orderings3.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -36,9 +34,9 @@ procedure P() returns () { } procedure Q() returns () { - + assert (forall x:Wicket :: x <: b && x != b ==> x <: c); // unprovable assert !(exists x:Wicket :: b <: x && b != x); // unprovable -} \ No newline at end of file +} diff --git a/Test/test21/Orderings3.bpl.a.expect b/Test/test21/Orderings3.bpl.a.expect index 3efb7e012..32f45b4b2 100644 --- a/Test/test21/Orderings3.bpl.a.expect +++ b/Test/test21/Orderings3.bpl.a.expect @@ -1,11 +1,11 @@ -Orderings3.bpl(35,3): Error BP5001: This assertion might not hold. +Orderings3.bpl(33,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings3.bpl(21,3): anon0 -Orderings3.bpl(40,3): Error BP5001: This assertion might not hold. + Orderings3.bpl(19,3): anon0 +Orderings3.bpl(38,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings3.bpl(40,3): anon0 -Orderings3.bpl(42,3): Error BP5001: This assertion might not hold. + Orderings3.bpl(38,3): anon0 +Orderings3.bpl(40,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings3.bpl(40,3): anon0 + Orderings3.bpl(38,3): anon0 Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Orderings3.bpl.n.expect b/Test/test21/Orderings3.bpl.n.expect deleted file mode 100644 index 3efb7e012..000000000 --- a/Test/test21/Orderings3.bpl.n.expect +++ /dev/null @@ -1,11 +0,0 @@ -Orderings3.bpl(35,3): Error BP5001: This assertion might not hold. -Execution trace: - Orderings3.bpl(21,3): anon0 -Orderings3.bpl(40,3): Error BP5001: This assertion might not hold. -Execution trace: - Orderings3.bpl(40,3): anon0 -Orderings3.bpl(42,3): Error BP5001: This assertion might not hold. -Execution trace: - Orderings3.bpl(40,3): anon0 - -Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Orderings3.bpl.p.expect b/Test/test21/Orderings3.bpl.p.expect index 3efb7e012..32f45b4b2 100644 --- a/Test/test21/Orderings3.bpl.p.expect +++ b/Test/test21/Orderings3.bpl.p.expect @@ -1,11 +1,11 @@ -Orderings3.bpl(35,3): Error BP5001: This assertion might not hold. +Orderings3.bpl(33,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings3.bpl(21,3): anon0 -Orderings3.bpl(40,3): Error BP5001: This assertion might not hold. + Orderings3.bpl(19,3): anon0 +Orderings3.bpl(38,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings3.bpl(40,3): anon0 -Orderings3.bpl(42,3): Error BP5001: This assertion might not hold. + Orderings3.bpl(38,3): anon0 +Orderings3.bpl(40,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings3.bpl(40,3): anon0 + Orderings3.bpl(38,3): anon0 Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Orderings4.bpl b/Test/test21/Orderings4.bpl index 9b4bbf0ac..d59e79766 100644 --- a/Test/test21/Orderings4.bpl +++ b/Test/test21/Orderings4.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -14,4 +12,4 @@ const unique s, t: Wicket extends unique r; procedure P() returns () { assert (forall x:Wicket, y:Wicket :: x <: s && y <: t ==> x != y); assert false; // unprovable -} \ No newline at end of file +} diff --git a/Test/test21/Orderings4.bpl.a.expect b/Test/test21/Orderings4.bpl.a.expect index 769f76b48..07aa60c8d 100644 --- a/Test/test21/Orderings4.bpl.a.expect +++ b/Test/test21/Orderings4.bpl.a.expect @@ -1,5 +1,5 @@ -Orderings4.bpl(16,3): Error BP5001: This assertion might not hold. +Orderings4.bpl(14,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings4.bpl(15,3): anon0 + Orderings4.bpl(13,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings4.bpl.n.expect b/Test/test21/Orderings4.bpl.n.expect deleted file mode 100644 index 769f76b48..000000000 --- a/Test/test21/Orderings4.bpl.n.expect +++ /dev/null @@ -1,5 +0,0 @@ -Orderings4.bpl(16,3): Error BP5001: This assertion might not hold. -Execution trace: - Orderings4.bpl(15,3): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings4.bpl.p.expect b/Test/test21/Orderings4.bpl.p.expect index 769f76b48..07aa60c8d 100644 --- a/Test/test21/Orderings4.bpl.p.expect +++ b/Test/test21/Orderings4.bpl.p.expect @@ -1,5 +1,5 @@ -Orderings4.bpl(16,3): Error BP5001: This assertion might not hold. +Orderings4.bpl(14,3): Error BP5001: This assertion might not hold. Execution trace: - Orderings4.bpl(15,3): anon0 + Orderings4.bpl(13,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/ParallelAssignment.bpl b/Test/test21/ParallelAssignment.bpl index 8ff3b1dec..12ea36efe 100644 --- a/Test/test21/ParallelAssignment.bpl +++ b/Test/test21/ParallelAssignment.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -59,4 +57,4 @@ procedure Q() returns () modifies x, y, z; { assert a[x] == a[y]; // error -} \ No newline at end of file +} diff --git a/Test/test21/ParallelAssignment.bpl.a.expect b/Test/test21/ParallelAssignment.bpl.a.expect index 7334a3f4f..0318be2ee 100644 --- a/Test/test21/ParallelAssignment.bpl.a.expect +++ b/Test/test21/ParallelAssignment.bpl.a.expect @@ -1,11 +1,11 @@ -ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold. +ParallelAssignment.bpl(30,3): Error BP5001: This assertion might not hold. Execution trace: - ParallelAssignment.bpl(21,5): anon0 -ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold. + ParallelAssignment.bpl(19,5): anon0 +ParallelAssignment.bpl(39,3): Error BP5001: This assertion might not hold. Execution trace: - ParallelAssignment.bpl(21,5): anon0 -ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold. + ParallelAssignment.bpl(19,5): anon0 +ParallelAssignment.bpl(58,3): Error BP5001: This assertion might not hold. Execution trace: - ParallelAssignment.bpl(46,11): anon0 + ParallelAssignment.bpl(44,11): anon0 Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/ParallelAssignment.bpl.n.expect b/Test/test21/ParallelAssignment.bpl.n.expect deleted file mode 100644 index 7334a3f4f..000000000 --- a/Test/test21/ParallelAssignment.bpl.n.expect +++ /dev/null @@ -1,11 +0,0 @@ -ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold. -Execution trace: - ParallelAssignment.bpl(21,5): anon0 -ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold. -Execution trace: - ParallelAssignment.bpl(21,5): anon0 -ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold. -Execution trace: - ParallelAssignment.bpl(46,11): anon0 - -Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/ParallelAssignment.bpl.p.expect b/Test/test21/ParallelAssignment.bpl.p.expect index 7334a3f4f..0318be2ee 100644 --- a/Test/test21/ParallelAssignment.bpl.p.expect +++ b/Test/test21/ParallelAssignment.bpl.p.expect @@ -1,11 +1,11 @@ -ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold. +ParallelAssignment.bpl(30,3): Error BP5001: This assertion might not hold. Execution trace: - ParallelAssignment.bpl(21,5): anon0 -ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold. + ParallelAssignment.bpl(19,5): anon0 +ParallelAssignment.bpl(39,3): Error BP5001: This assertion might not hold. Execution trace: - ParallelAssignment.bpl(21,5): anon0 -ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold. + ParallelAssignment.bpl(19,5): anon0 +ParallelAssignment.bpl(58,3): Error BP5001: This assertion might not hold. Execution trace: - ParallelAssignment.bpl(46,11): anon0 + ParallelAssignment.bpl(44,11): anon0 Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/PolyList.bpl b/Test/test21/PolyList.bpl index f7ff40d63..54d8f7451 100644 --- a/Test/test21/PolyList.bpl +++ b/Test/test21/PolyList.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -65,4 +63,4 @@ procedure Q() returns () { assert Len(Cons(1,Cons(2,Cons(3,NIL)))) == 2; // should not be provable -} \ No newline at end of file +} diff --git a/Test/test21/PolyList.bpl.a.expect b/Test/test21/PolyList.bpl.a.expect index 26132ce34..a54d06619 100644 --- a/Test/test21/PolyList.bpl.a.expect +++ b/Test/test21/PolyList.bpl.a.expect @@ -1,8 +1,8 @@ -PolyList.bpl(48,3): Error BP5001: This assertion might not hold. +PolyList.bpl(46,3): Error BP5001: This assertion might not hold. Execution trace: - PolyList.bpl(33,7): anon0 -PolyList.bpl(66,3): Error BP5001: This assertion might not hold. + PolyList.bpl(31,7): anon0 +PolyList.bpl(64,3): Error BP5001: This assertion might not hold. Execution trace: - PolyList.bpl(55,7): anon0 + PolyList.bpl(53,7): anon0 Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/PolyList.bpl.n.expect b/Test/test21/PolyList.bpl.n.expect deleted file mode 100644 index 26132ce34..000000000 --- a/Test/test21/PolyList.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -PolyList.bpl(48,3): Error BP5001: This assertion might not hold. -Execution trace: - PolyList.bpl(33,7): anon0 -PolyList.bpl(66,3): Error BP5001: This assertion might not hold. -Execution trace: - PolyList.bpl(55,7): anon0 - -Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/PolyList.bpl.p.expect b/Test/test21/PolyList.bpl.p.expect index 26132ce34..a54d06619 100644 --- a/Test/test21/PolyList.bpl.p.expect +++ b/Test/test21/PolyList.bpl.p.expect @@ -1,8 +1,8 @@ -PolyList.bpl(48,3): Error BP5001: This assertion might not hold. +PolyList.bpl(46,3): Error BP5001: This assertion might not hold. Execution trace: - PolyList.bpl(33,7): anon0 -PolyList.bpl(66,3): Error BP5001: This assertion might not hold. + PolyList.bpl(31,7): anon0 +PolyList.bpl(64,3): Error BP5001: This assertion might not hold. Execution trace: - PolyList.bpl(55,7): anon0 + PolyList.bpl(53,7): anon0 Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl index 584fb77bd..32732f6cc 100644 --- a/Test/test21/Real.bpl +++ b/Test/test21/Real.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -27,7 +25,7 @@ procedure ManyDigitReals() var x: real; var y: real; x := 15e-1; - y := real(3); + y := real(3); if (*) { assert x == y / 2000000000000000000000000001e-27; // error } else { diff --git a/Test/test21/Real.bpl.a.expect b/Test/test21/Real.bpl.a.expect index 9b8dc4f19..eaf8e9de3 100644 --- a/Test/test21/Real.bpl.a.expect +++ b/Test/test21/Real.bpl.a.expect @@ -1,10 +1,10 @@ -Real.bpl(32,5): Error BP5001: This assertion might not hold. +Real.bpl(30,5): Error BP5001: This assertion might not hold. Execution trace: - Real.bpl(29,5): anon0 - Real.bpl(32,5): anon3_Then -Real.bpl(47,5): Error BP5001: This assertion might not hold. + Real.bpl(27,5): anon0 + Real.bpl(30,5): anon3_Then +Real.bpl(45,5): Error BP5001: This assertion might not hold. Execution trace: - Real.bpl(40,3): anon0 - Real.bpl(47,5): anon3_Else + Real.bpl(38,3): anon0 + Real.bpl(45,5): anon3_Else Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/Real.bpl.n.expect b/Test/test21/Real.bpl.n.expect deleted file mode 100644 index 9b8dc4f19..000000000 --- a/Test/test21/Real.bpl.n.expect +++ /dev/null @@ -1,10 +0,0 @@ -Real.bpl(32,5): Error BP5001: This assertion might not hold. -Execution trace: - Real.bpl(29,5): anon0 - Real.bpl(32,5): anon3_Then -Real.bpl(47,5): Error BP5001: This assertion might not hold. -Execution trace: - Real.bpl(40,3): anon0 - Real.bpl(47,5): anon3_Else - -Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/Real.bpl.p.expect b/Test/test21/Real.bpl.p.expect index 9b8dc4f19..eaf8e9de3 100644 --- a/Test/test21/Real.bpl.p.expect +++ b/Test/test21/Real.bpl.p.expect @@ -1,10 +1,10 @@ -Real.bpl(32,5): Error BP5001: This assertion might not hold. +Real.bpl(30,5): Error BP5001: This assertion might not hold. Execution trace: - Real.bpl(29,5): anon0 - Real.bpl(32,5): anon3_Then -Real.bpl(47,5): Error BP5001: This assertion might not hold. + Real.bpl(27,5): anon0 + Real.bpl(30,5): anon3_Then +Real.bpl(45,5): Error BP5001: This assertion might not hold. Execution trace: - Real.bpl(40,3): anon0 - Real.bpl(47,5): anon3_Else + Real.bpl(38,3): anon0 + Real.bpl(45,5): anon3_Else Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/Triggers0.bpl b/Test/test21/Triggers0.bpl index c4b610f24..00462e63a 100644 --- a/Test/test21/Triggers0.bpl +++ b/Test/test21/Triggers0.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -47,4 +45,4 @@ procedure Q(x : a) returns () { assume o(x) == o(x); assert someConst == 42; assert someConst == 43; // should not be provable -} \ No newline at end of file +} diff --git a/Test/test21/Triggers0.bpl.a.expect b/Test/test21/Triggers0.bpl.a.expect index 44c7c84c0..14f5fa669 100644 --- a/Test/test21/Triggers0.bpl.a.expect +++ b/Test/test21/Triggers0.bpl.a.expect @@ -1,8 +1,8 @@ -Triggers0.bpl(45,3): Error BP5001: This assertion might not hold. +Triggers0.bpl(43,3): Error BP5001: This assertion might not hold. Execution trace: - Triggers0.bpl(45,3): anon0 -Triggers0.bpl(49,3): Error BP5001: This assertion might not hold. + Triggers0.bpl(43,3): anon0 +Triggers0.bpl(47,3): Error BP5001: This assertion might not hold. Execution trace: - Triggers0.bpl(45,3): anon0 + Triggers0.bpl(43,3): anon0 Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/test21/Triggers0.bpl.n.expect b/Test/test21/Triggers0.bpl.n.expect deleted file mode 100644 index 44c7c84c0..000000000 --- a/Test/test21/Triggers0.bpl.n.expect +++ /dev/null @@ -1,8 +0,0 @@ -Triggers0.bpl(45,3): Error BP5001: This assertion might not hold. -Execution trace: - Triggers0.bpl(45,3): anon0 -Triggers0.bpl(49,3): Error BP5001: This assertion might not hold. -Execution trace: - Triggers0.bpl(45,3): anon0 - -Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/test21/Triggers0.bpl.p.expect b/Test/test21/Triggers0.bpl.p.expect index 44c7c84c0..14f5fa669 100644 --- a/Test/test21/Triggers0.bpl.p.expect +++ b/Test/test21/Triggers0.bpl.p.expect @@ -1,8 +1,8 @@ -Triggers0.bpl(45,3): Error BP5001: This assertion might not hold. +Triggers0.bpl(43,3): Error BP5001: This assertion might not hold. Execution trace: - Triggers0.bpl(45,3): anon0 -Triggers0.bpl(49,3): Error BP5001: This assertion might not hold. + Triggers0.bpl(43,3): anon0 +Triggers0.bpl(47,3): Error BP5001: This assertion might not hold. Execution trace: - Triggers0.bpl(45,3): anon0 + Triggers0.bpl(43,3): anon0 Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/test21/Triggers1.bpl b/Test/test21/Triggers1.bpl index 3d8c95aff..fa8682636 100644 --- a/Test/test21/Triggers1.bpl +++ b/Test/test21/Triggers1.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" @@ -20,4 +18,4 @@ procedure P() returns () { assert g(x); assert g(m[x]); assert f(true); // should not be provable -} \ No newline at end of file +} diff --git a/Test/test21/Triggers1.bpl.a.expect b/Test/test21/Triggers1.bpl.a.expect index 817ddf319..b545248db 100644 --- a/Test/test21/Triggers1.bpl.a.expect +++ b/Test/test21/Triggers1.bpl.a.expect @@ -1,5 +1,5 @@ -Triggers1.bpl(22,3): Error BP5001: This assertion might not hold. +Triggers1.bpl(20,3): Error BP5001: This assertion might not hold. Execution trace: - Triggers1.bpl(18,3): anon0 + Triggers1.bpl(16,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Triggers1.bpl.n.expect b/Test/test21/Triggers1.bpl.n.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/test21/Triggers1.bpl.n.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Triggers1.bpl.p.expect b/Test/test21/Triggers1.bpl.p.expect index 817ddf319..b545248db 100644 --- a/Test/test21/Triggers1.bpl.p.expect +++ b/Test/test21/Triggers1.bpl.p.expect @@ -1,5 +1,5 @@ -Triggers1.bpl(22,3): Error BP5001: This assertion might not hold. +Triggers1.bpl(20,3): Error BP5001: This assertion might not hold. Execution trace: - Triggers1.bpl(18,3): anon0 + Triggers1.bpl(16,3): anon0 Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/test3_AddMethod_conv.bpl b/Test/test21/test3_AddMethod_conv.bpl index beb848f09..96ff02e15 100644 --- a/Test/test21/test3_AddMethod_conv.bpl +++ b/Test/test21/test3_AddMethod_conv.bpl @@ -1,5 +1,3 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" // RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" // RUN: %diff "%s.p.expect" "%t" // RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"