diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 4b99efb6aef..e7a4fa61120 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -711,7 +711,10 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran.OldAt(e.AtLabel), ISALLOC, true); if (wh != null) { var pIdx = e.Args.Count == 1 ? "" : " at index " + i; - var desc = new PODesc.IsAllocated($"argument{pIdx} ('{formal.Name}')", "in the two-state function's previous state"); + var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'", + "in the two-state function's previous state" + + PODesc.IsAllocated.HelperFormal(formal) + ); builder.Add(Assert(GetToken(ee), wh, desc)); } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 79dd1e2b157..0b7db48a7e3 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -477,7 +477,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis olderInParams.Add(bv); args.Add(formal); // add well-typedness conjunct to antecedent - Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, p.IsOld ? etran.Old : etran, NOALLOC); + Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, p.IsOld ? etran.Old : etran, ISALLOC); if (wh != null) { ante = BplAnd(ante, wh); } wh = GetWhereClause(p.tok, formal, p.Type, p.IsOld ? etranHeap.Old : etranHeap, ISALLOC); if (wh != null) { anteIsAlloc = BplAnd(anteIsAlloc, wh); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index d85264a3933..d5a46ab2890 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -1668,7 +1668,9 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { if (formal.IsOld) { var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal); var pIdx = m.Ins.Count == 1 ? "" : " at index " + index; - var desc = new PODesc.IsAllocated($"parameter{pIdx} ('{formal.Name}')", "in the two-state lemma's previous state"); + var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'", + "in the two-state lemma's previous state" + + PODesc.IsAllocated.HelperFormal(formal)); var require = Requires(formal.tok, false, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap), desc.FailureDescription, desc.SuccessDescription, null); require.Description = desc; diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 1727d05ffdf..b7cf77f1ace 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -1903,7 +1903,10 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran.OldAt(atLabel), ISALLOC, true); if (wh != null) { var pIdx = Args.Count == 1 ? "" : " at index " + i; - var desc = new PODesc.IsAllocated($"parameter{pIdx} ('{formal.Name}')", "in the two-state lemma's previous state"); + var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'", + "in the two-state lemma's previous state" + + PODesc.IsAllocated.HelperFormal(formal) + ); builder.Add(Assert(ee.tok, wh, desc)); } } diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index 87ebad91fa4..4cff0ae159c 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -260,7 +260,7 @@ public class IsAllocated : ProofObligationDescription { $"{PluralSuccess}{what} is always allocated{WhenSuffix}"; public override string FailureDescription => - $"{PluralFailure}{what} might not be allocated{WhenSuffix}"; + $"{PluralFailure}{what} could not be proved to be allocated{WhenSuffix}"; public override string ShortDescription => $"{what} allocated"; @@ -271,6 +271,11 @@ public class IsAllocated : ProofObligationDescription { private string PluralSuccess => plural ? "each " : ""; private string PluralFailure => plural ? "some " : ""; + public static string HelperFormal(Formal formal) { + return $" -- if you add 'new' before the parameter declaration, like 'new {formal.Name}: {formal.Type.ToString()}'," + + " arguments can refer to expressions possibly unallocated in the previous state"; + } + public IsAllocated(string what, string when, bool plural = false) { this.what = what; this.when = when; diff --git a/Source/DafnyDriver.Test/LanguageServerProcessTest.cs b/Source/DafnyDriver.Test/LanguageServerProcessTest.cs index ae8412e686c..d42c8f4d26a 100644 --- a/Source/DafnyDriver.Test/LanguageServerProcessTest.cs +++ b/Source/DafnyDriver.Test/LanguageServerProcessTest.cs @@ -79,7 +79,7 @@ public async Task LanguageServerStaysAliveIfParentDiesButNoParentIdWasProvided() } } - [Fact(Timeout = 10_000)] + [Fact(Timeout = 20_000)] public async Task LanguageServerShutsDownIfParentDies() { var process = await StartLanguageServerRunnerProcess(); diff --git a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs index 2121404e5a7..52930891a44 100644 --- a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs @@ -36,7 +36,7 @@ protected override Task SetUp(Action modifyOptions) { /// [Fact] public async Task QuickEditsInLargeFile() { - string GetLineContent(int index) => $"method Foo{index}() {{ assume false; }}"; + string GetLineContent(int index) => $"method Foo{index}() {{ assume {{:axiom}} false; }}"; var contentBuilder = new StringBuilder(); for (int lineNumber = 0; lineNumber < 1000; lineNumber++) { contentBuilder.AppendLine(GetLineContent(lineNumber)); diff --git a/Source/DafnyPipeline.Test/ProverLogStability.cs b/Source/DafnyPipeline.Test/ProverLogStability.cs index 137cbd79221..b2f3ae56d14 100644 --- a/Source/DafnyPipeline.Test/ProverLogStability.cs +++ b/Source/DafnyPipeline.Test/ProverLogStability.cs @@ -86,6 +86,8 @@ public ProverLogStabilityTest(ITestOutputHelper testOutputHelper) { this.testOutputHelper = testOutputHelper; } + private static bool updateProverLog = false; // Should always be false in committed code + /// /// This test is meant to detect _any_ changes in Dafny's verification behavior. /// Dafny's verification is powered by an SMT solver. For difficult inputs, such solvers may change their behavior, @@ -97,12 +99,14 @@ public ProverLogStabilityTest(ITestOutputHelper testOutputHelper) { /// /// If this test fails, that means a change was made to Dafny that changes the SMT input it sends. /// If this was intentional, you should update this test's expect file with the new SMT input. + /// To do so, set the static field above "updateProverLog" to true, run this test, set the flag back to false, and + /// run the test again to verify it works. /// The git history of updates to this test allows us to easily see when Dafny's verification has changed. /// /// If you make a change to Dafny verification and this test does not fail, then likely the Dafny code in the test /// does not sufficiently cover the language to detect your change. In that case, please update the test so it does. /// - /// Note that this test does not detect changes in DafnyPrelude.bplf + /// Note that this test does not detect changes in DafnyPrelude.bpl /// /// [Fact] @@ -111,8 +115,16 @@ public async Task ProverLogRegression() { var filePath = Path.Combine(Directory.GetCurrentDirectory(), "expectedProverLog.smt2"); var expectation = await File.ReadAllTextAsync(filePath); + expectation = expectation.Replace("\r", ""); var regularProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, originalProgram)); - Assert.Equal(expectation.Replace("\r", ""), regularProverLog.Replace("\r", "")); + regularProverLog = regularProverLog.Replace("\r", ""); + if (updateProverLog) { + var path = Path.GetFullPath(filePath).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, ""); + await File.WriteAllTextAsync(path, regularProverLog); + await Console.Out.WriteLineAsync("Updated prover log file at " + path); + } else { + Assert.Equal(expectation, regularProverLog); + } } private async Task GetProverLogForProgramAsync(DafnyOptions options, IEnumerable boogiePrograms) { diff --git a/Source/DafnyPipeline.Test/expectedProverLog.smt2 b/Source/DafnyPipeline.Test/expectedProverLog.smt2 index 98d5aff9366..99a6869bf00 100644 --- a/Source/DafnyPipeline.Test/expectedProverLog.smt2 +++ b/Source/DafnyPipeline.Test/expectedProverLog.smt2 @@ -304,13 +304,13 @@ $generated@@157))) (declare-fun $generated@@85 (Int) Int) (declare-fun $generated@@87 (T@T T@U) T@U) (declare-fun $generated@@90 (T@T T@U) T@U) -(declare-fun $generated@@93 () Int) -(declare-fun $generated@@94 (T@U Int T@U) Int) -(declare-fun $generated@@95 (T@U Int T@U) Bool) -(declare-fun $generated@@96 (T@U) Bool) -(declare-fun $generated@@103 (T@U T@U) Bool) -(declare-fun $generated@@115 (T@U T@U) T@U) -(declare-fun $generated@@122 (T@U) T@U) +(declare-fun $generated@@94 (T@U) Bool) +(declare-fun $generated@@97 (T@U T@U) Bool) +(declare-fun $generated@@109 (T@U T@U) T@U) +(declare-fun $generated@@116 (T@U) T@U) +(declare-fun $generated@@125 () Int) +(declare-fun $generated@@126 (T@U Int T@U) Int) +(declare-fun $generated@@127 (T@U Int T@U) Bool) (declare-fun $generated@@131 () T@U) (declare-fun $generated@@133 (T@U T@U) Bool) (declare-fun $generated@@137 (T@U) T@U) @@ -381,55 +381,55 @@ $generated@@157))) (assert (forall (($generated@@91 T@U) ($generated@@92 T@T) ) (! (= ($generated@@90 $generated@@92 ($generated@@56 $generated@@92 $generated@@91)) $generated@@91) :pattern ( ($generated@@56 $generated@@92 $generated@@91)) ))) -(assert (=> (<= 1 $generated@@93) (forall (($generated@@97 T@U) ($generated@@98 Int) ($generated@@99 T@U) ) (! (=> (or ($generated@@95 $generated@@97 $generated@@98 $generated@@99) (and (< 1 $generated@@93) (and ($generated@@96 $generated@@97) ($generated@@38 $generated@@39 $generated@@99 $generated@@46)))) (and (= ($generated@@94 $generated@@97 $generated@@98 $generated@@99) ($generated@@22 ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@97 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@97 $generated@@99) $generated@@52))) $generated@@55)))) (<= ($generated@@85 0) ($generated@@94 $generated@@97 $generated@@98 $generated@@99)))) - :pattern ( ($generated@@94 $generated@@97 $generated@@98 $generated@@99)) -)))) -(assert (forall (($generated@@100 T@U) ) (! (= ($generated@@38 $generated@@17 $generated@@100 $generated@@35) (<= ($generated@@85 0) ($generated@@22 $generated@@100))) - :pattern ( ($generated@@38 $generated@@17 $generated@@100 $generated@@35)) +(assert (forall (($generated@@93 T@U) ) (! (= ($generated@@38 $generated@@17 $generated@@93 $generated@@35) (<= ($generated@@85 0) ($generated@@22 $generated@@93))) + :pattern ( ($generated@@38 $generated@@17 $generated@@93 $generated@@35)) ))) (assert ($generated@@54 $generated@@1)) -(assert (forall (($generated@@101 T@U) ($generated@@102 T@U) ) (! (=> (and (and ($generated@@96 $generated@@101) (and (or (not (= $generated@@102 $generated@@41)) (not true)) (= ($generated@@42 $generated@@102) $generated@@44))) ($generated@@20 ($generated@@56 $generated@@16 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@101 $generated@@102) $generated@@1)))) ($generated@@34 $generated@@17 ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@101 $generated@@102) $generated@@55)) $generated $generated@@101)) - :pattern ( ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@101 $generated@@102) $generated@@55))) +(assert (forall (($generated@@95 T@U) ($generated@@96 T@U) ) (! (=> (and (and ($generated@@94 $generated@@95) (and (or (not (= $generated@@96 $generated@@41)) (not true)) (= ($generated@@42 $generated@@96) $generated@@44))) ($generated@@20 ($generated@@56 $generated@@16 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@95 $generated@@96) $generated@@1)))) ($generated@@34 $generated@@17 ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@95 $generated@@96) $generated@@55)) $generated $generated@@95)) + :pattern ( ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@95 $generated@@96) $generated@@55))) ))) -(assert (forall (($generated@@104 T@U) ($generated@@105 T@U) ) (! (= ($generated@@103 $generated@@104 $generated@@105) (forall (($generated@@106 T@U) ) (! (= ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@104 $generated@@106)) ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@105 $generated@@106))) - :pattern ( ($generated@@57 $generated@@59 $generated@@16 $generated@@104 $generated@@106)) - :pattern ( ($generated@@57 $generated@@59 $generated@@16 $generated@@105 $generated@@106)) +(assert (forall (($generated@@98 T@U) ($generated@@99 T@U) ) (! (= ($generated@@97 $generated@@98 $generated@@99) (forall (($generated@@100 T@U) ) (! (= ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@98 $generated@@100)) ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@99 $generated@@100))) + :pattern ( ($generated@@57 $generated@@59 $generated@@16 $generated@@98 $generated@@100)) + :pattern ( ($generated@@57 $generated@@59 $generated@@16 $generated@@99 $generated@@100)) ))) - :pattern ( ($generated@@103 $generated@@104 $generated@@105)) + :pattern ( ($generated@@97 $generated@@98 $generated@@99)) ))) -(assert (forall (($generated@@107 T@U) ($generated@@108 T@U) ) (! (=> (and ($generated@@96 $generated@@107) (and (or (not (= $generated@@108 $generated@@41)) (not true)) (= ($generated@@42 $generated@@108) $generated@@40))) ($generated@@38 $generated@@39 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@107 $generated@@108) $generated@@52)) $generated@@49)) - :pattern ( ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@107 $generated@@108) $generated@@52))) +(assert (forall (($generated@@101 T@U) ($generated@@102 T@U) ) (! (=> (and ($generated@@94 $generated@@101) (and (or (not (= $generated@@102 $generated@@41)) (not true)) (= ($generated@@42 $generated@@102) $generated@@40))) ($generated@@38 $generated@@39 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@101 $generated@@102) $generated@@52)) $generated@@49)) + :pattern ( ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@101 $generated@@102) $generated@@52))) ))) -(assert (forall (($generated@@109 T@U) ) (! (= ($generated@@38 $generated@@39 $generated@@109 $generated@@46) (and ($generated@@38 $generated@@39 $generated@@109 $generated@@40) (or (not (= $generated@@109 $generated@@41)) (not true)))) - :pattern ( ($generated@@38 $generated@@39 $generated@@109 $generated@@46)) +(assert (forall (($generated@@103 T@U) ) (! (= ($generated@@38 $generated@@39 $generated@@103 $generated@@46) (and ($generated@@38 $generated@@39 $generated@@103 $generated@@40) (or (not (= $generated@@103 $generated@@41)) (not true)))) + :pattern ( ($generated@@38 $generated@@39 $generated@@103 $generated@@46)) ))) -(assert (forall (($generated@@110 T@U) ) (! (= ($generated@@38 $generated@@39 $generated@@110 $generated@@49) (and ($generated@@38 $generated@@39 $generated@@110 $generated@@44) (or (not (= $generated@@110 $generated@@41)) (not true)))) - :pattern ( ($generated@@38 $generated@@39 $generated@@110 $generated@@49)) +(assert (forall (($generated@@104 T@U) ) (! (= ($generated@@38 $generated@@39 $generated@@104 $generated@@49) (and ($generated@@38 $generated@@39 $generated@@104 $generated@@44) (or (not (= $generated@@104 $generated@@41)) (not true)))) + :pattern ( ($generated@@38 $generated@@39 $generated@@104 $generated@@49)) ))) -(assert (forall (($generated@@111 T@U) ($generated@@112 T@U) ) (! (=> (and (and ($generated@@96 $generated@@111) (and (or (not (= $generated@@112 $generated@@41)) (not true)) (= ($generated@@42 $generated@@112) $generated@@40))) ($generated@@20 ($generated@@56 $generated@@16 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@111 $generated@@112) $generated@@1)))) ($generated@@34 $generated@@39 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@111 $generated@@112) $generated@@52)) $generated@@49 $generated@@111)) - :pattern ( ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@111 $generated@@112) $generated@@52))) +(assert (forall (($generated@@105 T@U) ($generated@@106 T@U) ) (! (=> (and (and ($generated@@94 $generated@@105) (and (or (not (= $generated@@106 $generated@@41)) (not true)) (= ($generated@@42 $generated@@106) $generated@@40))) ($generated@@20 ($generated@@56 $generated@@16 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@105 $generated@@106) $generated@@1)))) ($generated@@34 $generated@@39 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@105 $generated@@106) $generated@@52)) $generated@@49 $generated@@105)) + :pattern ( ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@105 $generated@@106) $generated@@52))) ))) -(assert (forall (($generated@@113 T@U) ($generated@@114 T@U) ) (! (=> ($generated@@103 $generated@@113 $generated@@114) (= $generated@@113 $generated@@114)) - :pattern ( ($generated@@103 $generated@@113 $generated@@114)) +(assert (forall (($generated@@107 T@U) ($generated@@108 T@U) ) (! (=> ($generated@@97 $generated@@107 $generated@@108) (= $generated@@107 $generated@@108)) + :pattern ( ($generated@@97 $generated@@107 $generated@@108)) ))) -(assert (forall (($generated@@116 T@U) ($generated@@117 T@U) ($generated@@118 T@U) ) (! (=> ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@116 $generated@@118)) ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 ($generated@@115 $generated@@116 $generated@@117) $generated@@118))) - :pattern ( ($generated@@115 $generated@@116 $generated@@117) ($generated@@57 $generated@@59 $generated@@16 $generated@@116 $generated@@118)) +(assert (forall (($generated@@110 T@U) ($generated@@111 T@U) ($generated@@112 T@U) ) (! (=> ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@110 $generated@@112)) ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 ($generated@@109 $generated@@110 $generated@@111) $generated@@112))) + :pattern ( ($generated@@109 $generated@@110 $generated@@111) ($generated@@57 $generated@@59 $generated@@16 $generated@@110 $generated@@112)) ))) -(assert (forall (($generated@@119 T@U) ($generated@@120 T@U) ($generated@@121 T@U) ) (! (= ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 ($generated@@115 $generated@@119 $generated@@120) $generated@@121)) (or (= $generated@@121 $generated@@120) ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@119 $generated@@121)))) - :pattern ( ($generated@@57 $generated@@59 $generated@@16 ($generated@@115 $generated@@119 $generated@@120) $generated@@121)) +(assert (forall (($generated@@113 T@U) ($generated@@114 T@U) ($generated@@115 T@U) ) (! (= ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 ($generated@@109 $generated@@113 $generated@@114) $generated@@115)) (or (= $generated@@115 $generated@@114) ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@113 $generated@@115)))) + :pattern ( ($generated@@57 $generated@@59 $generated@@16 ($generated@@109 $generated@@113 $generated@@114) $generated@@115)) ))) -(assert (forall (($generated@@123 T@U) ($generated@@124 T@U) ) (! (and (= ($generated@@122 ($generated@@53 $generated@@123 $generated@@124)) $generated@@123) (= ($generated@@33 ($generated@@53 $generated@@123 $generated@@124)) $generated@@124)) - :pattern ( ($generated@@53 $generated@@123 $generated@@124)) +(assert (forall (($generated@@117 T@U) ($generated@@118 T@U) ) (! (and (= ($generated@@116 ($generated@@53 $generated@@117 $generated@@118)) $generated@@117) (= ($generated@@33 ($generated@@53 $generated@@117 $generated@@118)) $generated@@118)) + :pattern ( ($generated@@53 $generated@@117 $generated@@118)) ))) -(assert (forall (($generated@@125 T@U) ($generated@@126 T@U) ) (! ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 ($generated@@115 $generated@@125 $generated@@126) $generated@@126)) - :pattern ( ($generated@@115 $generated@@125 $generated@@126)) +(assert (forall (($generated@@119 T@U) ($generated@@120 T@U) ) (! ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 ($generated@@109 $generated@@119 $generated@@120) $generated@@120)) + :pattern ( ($generated@@109 $generated@@119 $generated@@120)) ))) -(assert (forall (($generated@@127 T@U) ($generated@@128 T@T) ) (! (= ($generated@@56 $generated@@128 ($generated@@90 $generated@@128 $generated@@127)) $generated@@127) - :pattern ( ($generated@@90 $generated@@128 $generated@@127)) +(assert (forall (($generated@@121 T@U) ($generated@@122 T@T) ) (! (= ($generated@@56 $generated@@122 ($generated@@90 $generated@@122 $generated@@121)) $generated@@121) + :pattern ( ($generated@@90 $generated@@122 $generated@@121)) ))) -(assert (forall (($generated@@129 T@U) ($generated@@130 T@U) ) (! (=> (and ($generated@@96 $generated@@129) (and (or (not (= $generated@@130 $generated@@41)) (not true)) (= ($generated@@42 $generated@@130) $generated@@44))) ($generated@@38 $generated@@17 ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@129 $generated@@130) $generated@@55)) $generated)) - :pattern ( ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@129 $generated@@130) $generated@@55))) +(assert (forall (($generated@@123 T@U) ($generated@@124 T@U) ) (! (=> (and ($generated@@94 $generated@@123) (and (or (not (= $generated@@124 $generated@@41)) (not true)) (= ($generated@@42 $generated@@124) $generated@@44))) ($generated@@38 $generated@@17 ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@123 $generated@@124) $generated@@55)) $generated)) + :pattern ( ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@123 $generated@@124) $generated@@55))) ))) +(assert (=> (<= 1 $generated@@125) (forall (($generated@@128 T@U) ($generated@@129 Int) ($generated@@130 T@U) ) (! (=> (or ($generated@@127 $generated@@128 $generated@@129 $generated@@130) (and (< 1 $generated@@125) (and ($generated@@94 $generated@@128) (and ($generated@@38 $generated@@39 $generated@@130 $generated@@46) ($generated@@34 $generated@@39 $generated@@130 $generated@@46 $generated@@128))))) (and (= ($generated@@126 $generated@@128 $generated@@129 $generated@@130) ($generated@@22 ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@128 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@128 $generated@@130) $generated@@52))) $generated@@55)))) (<= ($generated@@85 0) ($generated@@126 $generated@@128 $generated@@129 $generated@@130)))) + :pattern ( ($generated@@126 $generated@@128 $generated@@129 $generated@@130)) +)))) (assert (forall (($generated@@132 T@U) ) (! (not ($generated@@20 ($generated@@57 $generated@@59 $generated@@16 $generated@@131 $generated@@132))) :pattern ( ($generated@@57 $generated@@59 $generated@@16 $generated@@131 $generated@@132)) ))) @@ -465,8 +465,8 @@ $generated@@157))) (assert (forall (($generated@@174 T@U) ($generated@@175 T@T) ) (! (= ($generated@@90 $generated@@175 ($generated@@87 $generated@@175 $generated@@174)) ($generated@@87 $generated@@59 ($generated@@90 $generated@@175 $generated@@174))) :pattern ( ($generated@@90 $generated@@175 ($generated@@87 $generated@@175 $generated@@174))) ))) -(assert (=> (<= 1 $generated@@93) (forall (($generated@@176 T@U) ($generated@@177 Int) ($generated@@178 T@U) ) (! (=> (or ($generated@@95 $generated@@176 $generated@@177 $generated@@178) (and (< 1 $generated@@93) (and ($generated@@96 $generated@@176) ($generated@@38 $generated@@39 $generated@@178 $generated@@46)))) (= ($generated@@94 $generated@@176 $generated@@177 $generated@@178) ($generated@@85 3))) - :pattern ( ($generated@@94 $generated@@176 $generated@@177 $generated@@178) ($generated@@96 $generated@@176)) +(assert (=> (<= 1 $generated@@125) (forall (($generated@@176 T@U) ($generated@@177 Int) ($generated@@178 T@U) ) (! (=> (or ($generated@@127 $generated@@176 $generated@@177 $generated@@178) (and (< 1 $generated@@125) (and ($generated@@94 $generated@@176) ($generated@@38 $generated@@39 $generated@@178 $generated@@46)))) (= ($generated@@126 $generated@@176 $generated@@177 $generated@@178) ($generated@@85 3))) + :pattern ( ($generated@@126 $generated@@176 $generated@@177 $generated@@178) ($generated@@94 $generated@@176)) )))) (assert (forall (($generated@@179 T@U) ($generated@@180 T@U) ) (! ($generated@@34 $generated@@17 $generated@@180 $generated $generated@@179) :pattern ( ($generated@@34 $generated@@17 $generated@@180 $generated $generated@@179)) @@ -497,11 +497,11 @@ $generated@@157))) (set-option :pp.bv_literals false) (set-option :smt.arith.solver 2) (assert (not - (=> (= (ControlFlow 0 0) 14) (let (($generated@@188 (=> (= (ControlFlow 0 7) (- 0 6)) (= ($generated@@94 $generated@@182 $generated@@183 $generated@@184) ($generated@@22 ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) $generated@@55))))))) -(let (($generated@@189 (and (=> (= (ControlFlow 0 8) (- 0 9)) ($generated@@38 $generated@@17 ($generated@@21 ($generated@@85 3)) $generated@@35)) (=> ($generated@@38 $generated@@17 ($generated@@21 ($generated@@85 3)) $generated@@35) (=> (= ($generated@@94 $generated@@182 $generated@@183 $generated@@184) ($generated@@85 3)) (=> (and ($generated@@38 $generated@@17 ($generated@@21 ($generated@@94 $generated@@182 $generated@@183 $generated@@184)) $generated@@35) (= (ControlFlow 0 8) 7)) $generated@@188)))))) -(let (($generated@@190 (=> (<= ($generated@@85 0) ($generated@@94 $generated@@182 $generated@@183 $generated@@184)) (=> (and ($generated@@34 $generated@@17 ($generated@@21 $generated@@183) $generated $generated@@182) ($generated@@34 $generated@@39 $generated@@184 $generated@@46 $generated@@182)) (and (=> (= (ControlFlow 0 2) (- 0 5)) (or (or (<= 0 $generated@@183) (and ($generated@@133 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (not ($generated@@133 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)))))) (= $generated@@183 $generated@@183))) (=> (or (or (<= 0 $generated@@183) (and ($generated@@133 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (not ($generated@@133 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)))))) (= $generated@@183 $generated@@183)) (and (=> (= (ControlFlow 0 2) (- 0 4)) (or (and (= $generated@@183 $generated@@183) (= $generated@@184 $generated@@184)) (or (and ($generated@@133 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (not ($generated@@133 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))))) (and ($generated@@103 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (or (< $generated@@183 $generated@@183) (and (= $generated@@183 $generated@@183) (and (= $generated@@184 $generated@@41) (or (not (= $generated@@184 $generated@@41)) (not true))))))))) (=> (or (and (= $generated@@183 $generated@@183) (= $generated@@184 $generated@@184)) (or (and ($generated@@133 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (not ($generated@@133 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))))) (and ($generated@@103 ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@115 ($generated@@115 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (or (< $generated@@183 $generated@@183) (and (= $generated@@183 $generated@@183) (and (= $generated@@184 $generated@@41) (or (not (= $generated@@184 $generated@@41)) (not true)))))))) (=> (or (and (= $generated@@183 $generated@@183) (= $generated@@184 $generated@@184)) ($generated@@95 $generated@@182 $generated@@183 $generated@@184)) (and (=> (= (ControlFlow 0 2) (- 0 3)) (or (not (= $generated@@184 $generated@@41)) (not true))) (=> (or (not (= $generated@@184 $generated@@41)) (not true)) (=> (= (ControlFlow 0 2) (- 0 1)) (or (not (= ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) $generated@@41)) (not true)))))))))))))) + (=> (= (ControlFlow 0 0) 14) (let (($generated@@188 (=> (= (ControlFlow 0 7) (- 0 6)) (= ($generated@@126 $generated@@182 $generated@@183 $generated@@184) ($generated@@22 ($generated@@56 $generated@@17 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) $generated@@55))))))) +(let (($generated@@189 (and (=> (= (ControlFlow 0 8) (- 0 9)) ($generated@@38 $generated@@17 ($generated@@21 ($generated@@85 3)) $generated@@35)) (=> ($generated@@38 $generated@@17 ($generated@@21 ($generated@@85 3)) $generated@@35) (=> (= ($generated@@126 $generated@@182 $generated@@183 $generated@@184) ($generated@@85 3)) (=> (and ($generated@@38 $generated@@17 ($generated@@21 ($generated@@126 $generated@@182 $generated@@183 $generated@@184)) $generated@@35) (= (ControlFlow 0 8) 7)) $generated@@188)))))) +(let (($generated@@190 (=> (<= ($generated@@85 0) ($generated@@126 $generated@@182 $generated@@183 $generated@@184)) (=> (and ($generated@@34 $generated@@17 ($generated@@21 $generated@@183) $generated $generated@@182) ($generated@@34 $generated@@39 $generated@@184 $generated@@46 $generated@@182)) (and (=> (= (ControlFlow 0 2) (- 0 5)) (or (or (<= 0 $generated@@183) (and ($generated@@133 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (not ($generated@@133 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)))))) (= $generated@@183 $generated@@183))) (=> (or (or (<= 0 $generated@@183) (and ($generated@@133 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (not ($generated@@133 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)))))) (= $generated@@183 $generated@@183)) (and (=> (= (ControlFlow 0 2) (- 0 4)) (or (and (= $generated@@183 $generated@@183) (= $generated@@184 $generated@@184)) (or (and ($generated@@133 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (not ($generated@@133 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))))) (and ($generated@@97 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (or (< $generated@@183 $generated@@183) (and (= $generated@@183 $generated@@183) (and (= $generated@@184 $generated@@41) (or (not (= $generated@@184 $generated@@41)) (not true))))))))) (=> (or (and (= $generated@@183 $generated@@183) (= $generated@@184 $generated@@184)) (or (and ($generated@@133 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (not ($generated@@133 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))))) (and ($generated@@97 ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) ($generated@@109 ($generated@@109 $generated@@131 ($generated@@90 $generated@@39 $generated@@184)) ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52))) (or (< $generated@@183 $generated@@183) (and (= $generated@@183 $generated@@183) (and (= $generated@@184 $generated@@41) (or (not (= $generated@@184 $generated@@41)) (not true)))))))) (=> (or (and (= $generated@@183 $generated@@183) (= $generated@@184 $generated@@184)) ($generated@@127 $generated@@182 $generated@@183 $generated@@184)) (and (=> (= (ControlFlow 0 2) (- 0 3)) (or (not (= $generated@@184 $generated@@41)) (not true))) (=> (or (not (= $generated@@184 $generated@@41)) (not true)) (=> (= (ControlFlow 0 2) (- 0 1)) (or (not (= ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)) $generated@@41)) (not true)))))))))))))) (let (($generated@@191 (=> (= $generated@@185 ($generated@@139 $generated@@41 $generated@@182 $generated@@1 $generated@@184 ($generated@@56 $generated@@39 ($generated@@57 $generated@@58 $generated@@59 ($generated@@57 $generated@@39 ($generated@@60 $generated@@58 $generated@@59) $generated@@182 $generated@@184) $generated@@52)))) (and (=> (= (ControlFlow 0 10) (- 0 13)) (or (not (= $generated@@184 $generated@@41)) (not true))) (=> (or (not (= $generated@@184 $generated@@41)) (not true)) (=> (= $generated@@186 ($generated@@20 ($generated@@138 $generated@@39 $generated@@58 $generated@@16 $generated@@185 $generated@@184 $generated@@52))) (and (=> (= (ControlFlow 0 10) (- 0 12)) $generated@@186) (=> $generated@@186 (and (=> (= (ControlFlow 0 10) (- 0 11)) (or (not (= $generated@@184 $generated@@41)) (not true))) (=> (or (not (= $generated@@184 $generated@@41)) (not true)) (and (=> (= (ControlFlow 0 10) 2) $generated@@190) (=> (= (ControlFlow 0 10) 8) $generated@@189)))))))))))) -(let (($generated@@192 (=> (and (and (and ($generated@@96 $generated@@182) ($generated@@187 $generated@@182)) ($generated@@38 $generated@@39 $generated@@184 $generated@@46)) (and (= 1 $generated@@93) (= (ControlFlow 0 14) 10))) $generated@@191))) +(let (($generated@@192 (=> (and (and (and ($generated@@94 $generated@@182) ($generated@@187 $generated@@182)) ($generated@@38 $generated@@39 $generated@@184 $generated@@46)) (and (= 1 $generated@@125) (= (ControlFlow 0 14) 10))) $generated@@191))) $generated@@192)))))) )) (check-sat) @@ -618,28 +618,28 @@ $generated@@192)))))) (declare-fun $generated@@157 (T@U Int T@U) Int) (declare-fun $generated@@158 (T@U Int T@U) Bool) (declare-fun $generated@@165 (T@T T@U) T@U) -(declare-fun $generated@@168 () Int) -(declare-fun $generated@@172 (Int) T@U) -(declare-fun $generated@@176 (T@U) T@U) -(declare-fun $generated@@179 (T@T T@U T@U) T@U) -(declare-fun $generated@@180 () T@T) -(declare-fun $generated@@186 (T@U T@U T@U) Bool) -(declare-fun $generated@@205 (T@U T@U) T@U) -(declare-fun $generated@@210 (T@U T@U) T@U) -(declare-fun $generated@@215 (T@U T@U T@U T@U T@U) T@U) -(declare-fun $generated@@216 (T@U T@U T@U) T@U) -(declare-fun $generated@@233 (T@U T@U T@U T@U T@U) Bool) -(declare-fun $generated@@239 (Bool) T@U) -(declare-fun $generated@@242 (T@U) T@U) -(declare-fun $generated@@267 (T@U) T@U) -(declare-fun $generated@@287 (T@U) T@U) -(declare-fun $generated@@290 (T@U) T@U) -(declare-fun $generated@@293 (T@U) T@U) -(declare-fun $generated@@296 (T@U) T@U) -(declare-fun $generated@@299 (T@U) T@U) +(declare-fun $generated@@168 (Int) T@U) +(declare-fun $generated@@172 (T@U) T@U) +(declare-fun $generated@@175 (T@T T@U T@U) T@U) +(declare-fun $generated@@176 () T@T) +(declare-fun $generated@@182 (T@U T@U T@U) Bool) +(declare-fun $generated@@201 (T@U T@U) T@U) +(declare-fun $generated@@206 (T@U T@U) T@U) +(declare-fun $generated@@211 (T@U T@U T@U T@U T@U) T@U) +(declare-fun $generated@@212 (T@U T@U T@U) T@U) +(declare-fun $generated@@229 (T@U T@U T@U T@U T@U) Bool) +(declare-fun $generated@@235 (Bool) T@U) +(declare-fun $generated@@238 (T@U) T@U) +(declare-fun $generated@@263 (T@U) T@U) +(declare-fun $generated@@283 (T@U) T@U) +(declare-fun $generated@@286 (T@U) T@U) +(declare-fun $generated@@289 (T@U) T@U) +(declare-fun $generated@@292 (T@U) T@U) +(declare-fun $generated@@295 (T@U) T@U) +(declare-fun $generated@@298 (T@U) T@U) (declare-fun $generated@@302 (T@U) T@U) -(declare-fun $generated@@306 (T@U) T@U) -(declare-fun $generated@@321 (T@U) T@U) +(declare-fun $generated@@317 (T@U) T@U) +(declare-fun $generated@@330 () Int) (declare-fun $generated@@335 (T@U T@U T@U Bool) T@U) (declare-fun $generated@@342 (T@U) T@U) (declare-fun $generated@@413 (T@U) T@U) @@ -742,176 +742,176 @@ $generated@@192)))))) (assert (forall (($generated@@166 T@U) ($generated@@167 T@T) ) (! (= ($generated@@165 $generated@@167 ($generated@@126 $generated@@167 $generated@@166)) $generated@@166) :pattern ( ($generated@@126 $generated@@167 $generated@@166)) ))) -(assert (=> (<= 1 $generated@@168) (forall (($generated@@169 T@U) ($generated@@170 Int) ($generated@@171 T@U) ) (! (=> (or ($generated@@158 $generated@@169 $generated@@170 $generated@@171) (and (< 1 $generated@@168) (and ($generated@@148 $generated@@169) ($generated@@98 $generated@@43 $generated@@171 $generated@@115)))) (and (= ($generated@@157 $generated@@169 $generated@@170 $generated@@171) ($generated@@29 ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@169 ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@169 $generated@@171) $generated@@121))) $generated@@124)))) (<= ($generated@@141 0) ($generated@@157 $generated@@169 $generated@@170 $generated@@171)))) - :pattern ( ($generated@@157 $generated@@169 $generated@@170 $generated@@171)) -)))) -(assert (forall (($generated@@173 Int) ($generated@@174 T@U) ($generated@@175 T@U) ) (! (= ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 $generated@@45 ($generated@@172 $generated@@173) $generated@@174 $generated@@175) ($generated@@165 $generated@@24 ($generated@@28 (+ ($generated@@29 ($generated@@126 $generated@@24 $generated@@175)) $generated@@173)))) - :pattern ( ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 $generated@@45 ($generated@@172 $generated@@173) $generated@@174 $generated@@175)) +(assert (forall (($generated@@169 Int) ($generated@@170 T@U) ($generated@@171 T@U) ) (! (= ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 $generated@@45 ($generated@@168 $generated@@169) $generated@@170 $generated@@171) ($generated@@165 $generated@@24 ($generated@@28 (+ ($generated@@29 ($generated@@126 $generated@@24 $generated@@171)) $generated@@169)))) + :pattern ( ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 $generated@@45 ($generated@@168 $generated@@169) $generated@@170 $generated@@171)) ))) -(assert (forall (($generated@@177 T@U) ($generated@@178 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@176 $generated@@177) $generated@@178)) ($generated@@27 ($generated@@49 $generated@@43 $generated@@23 $generated@@177 ($generated@@126 $generated@@43 $generated@@178)))) - :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@176 $generated@@177) $generated@@178)) +(assert (forall (($generated@@173 T@U) ($generated@@174 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@172 $generated@@173) $generated@@174)) ($generated@@27 ($generated@@49 $generated@@43 $generated@@23 $generated@@173 ($generated@@126 $generated@@43 $generated@@174)))) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@172 $generated@@173) $generated@@174)) ))) -(assert (= ($generated@@22 $generated@@180) 8)) -(assert (forall (($generated@@181 T@U) ($generated@@182 T@U) ($generated@@183 T@T) ) (! (= ($generated@@179 $generated@@183 $generated@@181 $generated@@182) ($generated@@49 $generated@@180 $generated@@183 $generated@@181 $generated@@182)) - :pattern ( ($generated@@179 $generated@@183 $generated@@181 $generated@@182)) +(assert (= ($generated@@22 $generated@@176) 8)) +(assert (forall (($generated@@177 T@U) ($generated@@178 T@U) ($generated@@179 T@T) ) (! (= ($generated@@175 $generated@@179 $generated@@177 $generated@@178) ($generated@@49 $generated@@176 $generated@@179 $generated@@177 $generated@@178)) + :pattern ( ($generated@@175 $generated@@179 $generated@@177 $generated@@178)) ))) (assert ($generated@@123 $generated@@2)) (assert ($generated@@148 $generated@@147)) -(assert (forall (($generated@@184 T@U) ($generated@@185 T@U) ) (! (=> (and (and ($generated@@148 $generated@@184) (and (or (not (= $generated@@185 $generated@@100)) (not true)) (= ($generated@@101 $generated@@185) $generated@@103))) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@184 $generated@@185) $generated@@2)))) ($generated@@114 $generated@@24 ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@184 $generated@@185) $generated@@124)) $generated $generated@@184)) - :pattern ( ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@184 $generated@@185) $generated@@124))) +(assert (forall (($generated@@180 T@U) ($generated@@181 T@U) ) (! (=> (and (and ($generated@@148 $generated@@180) (and (or (not (= $generated@@181 $generated@@100)) (not true)) (= ($generated@@101 $generated@@181) $generated@@103))) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@180 $generated@@181) $generated@@2)))) ($generated@@114 $generated@@24 ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@180 $generated@@181) $generated@@124)) $generated $generated@@180)) + :pattern ( ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@180 $generated@@181) $generated@@124))) ))) -(assert (forall (($generated@@187 T@U) ($generated@@188 T@U) ($generated@@189 T@U) ($generated@@190 T@T) ) (! (= ($generated@@186 ($generated@@165 $generated@@190 $generated@@187) $generated@@188 $generated@@189) ($generated@@114 $generated@@190 $generated@@187 $generated@@188 $generated@@189)) - :pattern ( ($generated@@186 ($generated@@165 $generated@@190 $generated@@187) $generated@@188 $generated@@189)) +(assert (forall (($generated@@183 T@U) ($generated@@184 T@U) ($generated@@185 T@U) ($generated@@186 T@T) ) (! (= ($generated@@182 ($generated@@165 $generated@@186 $generated@@183) $generated@@184 $generated@@185) ($generated@@114 $generated@@186 $generated@@183 $generated@@184 $generated@@185)) + :pattern ( ($generated@@182 ($generated@@165 $generated@@186 $generated@@183) $generated@@184 $generated@@185)) ))) -(assert (forall (($generated@@191 T@U) ($generated@@192 T@U) ($generated@@193 T@U) ($generated@@194 T@U) ) (! (=> ($generated@@133 $generated@@191 $generated@@192) (=> ($generated@@186 $generated@@193 $generated@@194 $generated@@191) ($generated@@186 $generated@@193 $generated@@194 $generated@@192))) - :pattern ( ($generated@@133 $generated@@191 $generated@@192) ($generated@@186 $generated@@193 $generated@@194 $generated@@191)) +(assert (forall (($generated@@187 T@U) ($generated@@188 T@U) ($generated@@189 T@U) ($generated@@190 T@U) ) (! (=> ($generated@@133 $generated@@187 $generated@@188) (=> ($generated@@182 $generated@@189 $generated@@190 $generated@@187) ($generated@@182 $generated@@189 $generated@@190 $generated@@188))) + :pattern ( ($generated@@133 $generated@@187 $generated@@188) ($generated@@182 $generated@@189 $generated@@190 $generated@@187)) ))) -(assert (forall (($generated@@195 T@U) ($generated@@196 T@U) ($generated@@197 T@U) ($generated@@198 T@U) ($generated@@199 T@T) ) (! (=> ($generated@@133 $generated@@195 $generated@@196) (=> ($generated@@114 $generated@@199 $generated@@197 $generated@@198 $generated@@195) ($generated@@114 $generated@@199 $generated@@197 $generated@@198 $generated@@196))) - :pattern ( ($generated@@133 $generated@@195 $generated@@196) ($generated@@114 $generated@@199 $generated@@197 $generated@@198 $generated@@195)) +(assert (forall (($generated@@191 T@U) ($generated@@192 T@U) ($generated@@193 T@U) ($generated@@194 T@U) ($generated@@195 T@T) ) (! (=> ($generated@@133 $generated@@191 $generated@@192) (=> ($generated@@114 $generated@@195 $generated@@193 $generated@@194 $generated@@191) ($generated@@114 $generated@@195 $generated@@193 $generated@@194 $generated@@192))) + :pattern ( ($generated@@133 $generated@@191 $generated@@192) ($generated@@114 $generated@@195 $generated@@193 $generated@@194 $generated@@191)) ))) -(assert (forall (($generated@@200 T@U) ($generated@@201 T@U) ) (! (= ($generated@@149 $generated@@200 $generated@@201) (forall (($generated@@202 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@200 $generated@@202)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@201 $generated@@202))) - :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@200 $generated@@202)) - :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@201 $generated@@202)) +(assert (forall (($generated@@196 T@U) ($generated@@197 T@U) ) (! (= ($generated@@149 $generated@@196 $generated@@197) (forall (($generated@@198 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@196 $generated@@198)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@197 $generated@@198))) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@196 $generated@@198)) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@197 $generated@@198)) ))) - :pattern ( ($generated@@149 $generated@@200 $generated@@201)) + :pattern ( ($generated@@149 $generated@@196 $generated@@197)) ))) -(assert (forall (($generated@@203 T@U) ($generated@@204 T@U) ) (! (=> (and ($generated@@148 $generated@@203) (and (or (not (= $generated@@204 $generated@@100)) (not true)) (= ($generated@@101 $generated@@204) $generated@@99))) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@203 $generated@@204) $generated@@121)) $generated@@118)) - :pattern ( ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@203 $generated@@204) $generated@@121))) +(assert (forall (($generated@@199 T@U) ($generated@@200 T@U) ) (! (=> (and ($generated@@148 $generated@@199) (and (or (not (= $generated@@200 $generated@@100)) (not true)) (= ($generated@@101 $generated@@200) $generated@@99))) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@199 $generated@@200) $generated@@121)) $generated@@118)) + :pattern ( ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@199 $generated@@200) $generated@@121))) ))) -(assert (forall (($generated@@206 T@U) ($generated@@207 T@U) ($generated@@208 T@U) ($generated@@209 T@U) ) (! (= ($generated@@114 $generated@@105 $generated@@208 ($generated@@205 $generated@@206 $generated@@207) $generated@@209) ($generated@@114 $generated@@105 $generated@@208 ($generated@@106 $generated@@206 $generated@@207) $generated@@209)) - :pattern ( ($generated@@114 $generated@@105 $generated@@208 ($generated@@205 $generated@@206 $generated@@207) $generated@@209)) +(assert (forall (($generated@@202 T@U) ($generated@@203 T@U) ($generated@@204 T@U) ($generated@@205 T@U) ) (! (= ($generated@@114 $generated@@105 $generated@@204 ($generated@@201 $generated@@202 $generated@@203) $generated@@205) ($generated@@114 $generated@@105 $generated@@204 ($generated@@106 $generated@@202 $generated@@203) $generated@@205)) + :pattern ( ($generated@@114 $generated@@105 $generated@@204 ($generated@@201 $generated@@202 $generated@@203) $generated@@205)) ))) -(assert (forall (($generated@@211 T@U) ($generated@@212 T@U) ($generated@@213 T@U) ($generated@@214 T@U) ) (! (= ($generated@@114 $generated@@105 $generated@@213 ($generated@@210 $generated@@211 $generated@@212) $generated@@214) ($generated@@114 $generated@@105 $generated@@213 ($generated@@205 $generated@@211 $generated@@212) $generated@@214)) - :pattern ( ($generated@@114 $generated@@105 $generated@@213 ($generated@@210 $generated@@211 $generated@@212) $generated@@214)) +(assert (forall (($generated@@207 T@U) ($generated@@208 T@U) ($generated@@209 T@U) ($generated@@210 T@U) ) (! (= ($generated@@114 $generated@@105 $generated@@209 ($generated@@206 $generated@@207 $generated@@208) $generated@@210) ($generated@@114 $generated@@105 $generated@@209 ($generated@@201 $generated@@207 $generated@@208) $generated@@210)) + :pattern ( ($generated@@114 $generated@@105 $generated@@209 ($generated@@206 $generated@@207 $generated@@208) $generated@@210)) ))) -(assert (forall (($generated@@217 T@U) ($generated@@218 T@U) ($generated@@219 T@U) ($generated@@220 T@U) ($generated@@221 T@U) ($generated@@222 T@U) ($generated@@223 T@U) ) (! (= ($generated@@215 $generated@@217 $generated@@218 $generated@@219 ($generated@@216 $generated@@220 $generated@@221 $generated@@222) $generated@@223) ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 $generated@@45 $generated@@220 $generated@@219 $generated@@223)) - :pattern ( ($generated@@215 $generated@@217 $generated@@218 $generated@@219 ($generated@@216 $generated@@220 $generated@@221 $generated@@222) $generated@@223)) +(assert (forall (($generated@@213 T@U) ($generated@@214 T@U) ($generated@@215 T@U) ($generated@@216 T@U) ($generated@@217 T@U) ($generated@@218 T@U) ($generated@@219 T@U) ) (! (= ($generated@@211 $generated@@213 $generated@@214 $generated@@215 ($generated@@212 $generated@@216 $generated@@217 $generated@@218) $generated@@219) ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 $generated@@45 $generated@@216 $generated@@215 $generated@@219)) + :pattern ( ($generated@@211 $generated@@213 $generated@@214 $generated@@215 ($generated@@212 $generated@@216 $generated@@217 $generated@@218) $generated@@219)) ))) -(assert (forall (($generated@@224 T@U) ) (! (=> ($generated@@47 $generated@@224 $generated@@125) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@224)) $generated@@224) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@224) $generated@@125))) - :pattern ( ($generated@@47 $generated@@224 $generated@@125)) +(assert (forall (($generated@@220 T@U) ) (! (=> ($generated@@47 $generated@@220 $generated@@125) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@220)) $generated@@220) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@220) $generated@@125))) + :pattern ( ($generated@@47 $generated@@220 $generated@@125)) ))) -(assert (forall (($generated@@225 T@U) ) (! (=> ($generated@@47 $generated@@225 $generated@@115) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@225)) $generated@@225) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@225) $generated@@115))) - :pattern ( ($generated@@47 $generated@@225 $generated@@115)) +(assert (forall (($generated@@221 T@U) ) (! (=> ($generated@@47 $generated@@221 $generated@@115) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@221)) $generated@@221) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@221) $generated@@115))) + :pattern ( ($generated@@47 $generated@@221 $generated@@115)) ))) -(assert (forall (($generated@@226 T@U) ) (! (=> ($generated@@47 $generated@@226 $generated@@99) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@226)) $generated@@226) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@226) $generated@@99))) - :pattern ( ($generated@@47 $generated@@226 $generated@@99)) +(assert (forall (($generated@@222 T@U) ) (! (=> ($generated@@47 $generated@@222 $generated@@99) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@222)) $generated@@222) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@222) $generated@@99))) + :pattern ( ($generated@@47 $generated@@222 $generated@@99)) ))) -(assert (forall (($generated@@227 T@U) ) (! (=> ($generated@@47 $generated@@227 $generated@@118) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@227)) $generated@@227) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@227) $generated@@118))) - :pattern ( ($generated@@47 $generated@@227 $generated@@118)) +(assert (forall (($generated@@223 T@U) ) (! (=> ($generated@@47 $generated@@223 $generated@@118) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@223)) $generated@@223) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@223) $generated@@118))) + :pattern ( ($generated@@47 $generated@@223 $generated@@118)) ))) -(assert (forall (($generated@@228 T@U) ) (! (=> ($generated@@47 $generated@@228 $generated@@103) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@228)) $generated@@228) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@228) $generated@@103))) - :pattern ( ($generated@@47 $generated@@228 $generated@@103)) +(assert (forall (($generated@@224 T@U) ) (! (=> ($generated@@47 $generated@@224 $generated@@103) (and (= ($generated@@165 $generated@@43 ($generated@@126 $generated@@43 $generated@@224)) $generated@@224) ($generated@@98 $generated@@43 ($generated@@126 $generated@@43 $generated@@224) $generated@@103))) + :pattern ( ($generated@@47 $generated@@224 $generated@@103)) ))) -(assert (forall (($generated@@229 T@U) ) (! (= ($generated@@98 $generated@@43 $generated@@229 $generated@@115) (and ($generated@@98 $generated@@43 $generated@@229 $generated@@99) (or (not (= $generated@@229 $generated@@100)) (not true)))) - :pattern ( ($generated@@98 $generated@@43 $generated@@229 $generated@@115)) +(assert (forall (($generated@@225 T@U) ) (! (= ($generated@@98 $generated@@43 $generated@@225 $generated@@115) (and ($generated@@98 $generated@@43 $generated@@225 $generated@@99) (or (not (= $generated@@225 $generated@@100)) (not true)))) + :pattern ( ($generated@@98 $generated@@43 $generated@@225 $generated@@115)) ))) -(assert (forall (($generated@@230 T@U) ) (! (= ($generated@@98 $generated@@43 $generated@@230 $generated@@118) (and ($generated@@98 $generated@@43 $generated@@230 $generated@@103) (or (not (= $generated@@230 $generated@@100)) (not true)))) - :pattern ( ($generated@@98 $generated@@43 $generated@@230 $generated@@118)) +(assert (forall (($generated@@226 T@U) ) (! (= ($generated@@98 $generated@@43 $generated@@226 $generated@@118) (and ($generated@@98 $generated@@43 $generated@@226 $generated@@103) (or (not (= $generated@@226 $generated@@100)) (not true)))) + :pattern ( ($generated@@98 $generated@@43 $generated@@226 $generated@@118)) ))) -(assert (forall (($generated@@231 T@U) ($generated@@232 T@U) ) (! (=> (and (and ($generated@@148 $generated@@231) (and (or (not (= $generated@@232 $generated@@100)) (not true)) (= ($generated@@101 $generated@@232) $generated@@99))) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@231 $generated@@232) $generated@@2)))) ($generated@@114 $generated@@43 ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@231 $generated@@232) $generated@@121)) $generated@@118 $generated@@231)) - :pattern ( ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@231 $generated@@232) $generated@@121))) +(assert (forall (($generated@@227 T@U) ($generated@@228 T@U) ) (! (=> (and (and ($generated@@148 $generated@@227) (and (or (not (= $generated@@228 $generated@@100)) (not true)) (= ($generated@@101 $generated@@228) $generated@@99))) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@227 $generated@@228) $generated@@2)))) ($generated@@114 $generated@@43 ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@227 $generated@@228) $generated@@121)) $generated@@118 $generated@@227)) + :pattern ( ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@227 $generated@@228) $generated@@121))) ))) -(assert (forall (($generated@@234 T@U) ($generated@@235 T@U) ($generated@@236 T@U) ($generated@@237 T@U) ) (! (=> (and ($generated@@148 $generated@@237) ($generated@@114 $generated@@105 $generated@@234 ($generated@@106 $generated@@235 $generated@@236) $generated@@237)) (forall (($generated@@238 T@U) ) (! (=> (and ($generated@@186 $generated@@238 $generated@@235 $generated@@237) ($generated@@233 $generated@@235 $generated@@236 $generated@@237 $generated@@234 $generated@@238)) ($generated@@186 ($generated@@215 $generated@@235 $generated@@236 $generated@@237 $generated@@234 $generated@@238) $generated@@236 $generated@@237)) - :pattern ( ($generated@@215 $generated@@235 $generated@@236 $generated@@237 $generated@@234 $generated@@238)) +(assert (forall (($generated@@230 T@U) ($generated@@231 T@U) ($generated@@232 T@U) ($generated@@233 T@U) ) (! (=> (and ($generated@@148 $generated@@233) ($generated@@114 $generated@@105 $generated@@230 ($generated@@106 $generated@@231 $generated@@232) $generated@@233)) (forall (($generated@@234 T@U) ) (! (=> (and ($generated@@182 $generated@@234 $generated@@231 $generated@@233) ($generated@@229 $generated@@231 $generated@@232 $generated@@233 $generated@@230 $generated@@234)) ($generated@@182 ($generated@@211 $generated@@231 $generated@@232 $generated@@233 $generated@@230 $generated@@234) $generated@@232 $generated@@233)) + :pattern ( ($generated@@211 $generated@@231 $generated@@232 $generated@@233 $generated@@230 $generated@@234)) ))) - :pattern ( ($generated@@114 $generated@@105 $generated@@234 ($generated@@106 $generated@@235 $generated@@236) $generated@@237)) + :pattern ( ($generated@@114 $generated@@105 $generated@@230 ($generated@@106 $generated@@231 $generated@@232) $generated@@233)) ))) -(assert (forall (($generated@@240 Bool) ($generated@@241 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@43 $generated@@23 ($generated@@239 $generated@@240) $generated@@241)) $generated@@240) - :pattern ( ($generated@@49 $generated@@43 $generated@@23 ($generated@@239 $generated@@240) $generated@@241)) +(assert (forall (($generated@@236 Bool) ($generated@@237 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@43 $generated@@23 ($generated@@235 $generated@@236) $generated@@237)) $generated@@236) + :pattern ( ($generated@@49 $generated@@43 $generated@@23 ($generated@@235 $generated@@236) $generated@@237)) ))) -(assert (forall (($generated@@243 T@U) ($generated@@244 T@U) ) (! (= ($generated@@49 $generated@@180 $generated@@105 ($generated@@242 $generated@@243) $generated@@244) $generated@@243) - :pattern ( ($generated@@49 $generated@@180 $generated@@105 ($generated@@242 $generated@@243) $generated@@244)) +(assert (forall (($generated@@239 T@U) ($generated@@240 T@U) ) (! (= ($generated@@49 $generated@@176 $generated@@105 ($generated@@238 $generated@@239) $generated@@240) $generated@@239) + :pattern ( ($generated@@49 $generated@@176 $generated@@105 ($generated@@238 $generated@@239) $generated@@240)) ))) -(assert (forall (($generated@@245 T@U) ($generated@@246 T@U) ($generated@@247 T@U) ) (! (= ($generated@@114 ($generated@@42 $generated@@45 $generated@@23) $generated@@245 ($generated@@137 $generated@@246) $generated@@247) (forall (($generated@@248 T@U) ) (! (=> ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@245 $generated@@248)) ($generated@@186 $generated@@248 $generated@@246 $generated@@247)) - :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@245 $generated@@248)) +(assert (forall (($generated@@241 T@U) ($generated@@242 T@U) ($generated@@243 T@U) ) (! (= ($generated@@114 ($generated@@42 $generated@@45 $generated@@23) $generated@@241 ($generated@@137 $generated@@242) $generated@@243) (forall (($generated@@244 T@U) ) (! (=> ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@241 $generated@@244)) ($generated@@182 $generated@@244 $generated@@242 $generated@@243)) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@241 $generated@@244)) ))) - :pattern ( ($generated@@114 ($generated@@42 $generated@@45 $generated@@23) $generated@@245 ($generated@@137 $generated@@246) $generated@@247)) + :pattern ( ($generated@@114 ($generated@@42 $generated@@45 $generated@@23) $generated@@241 ($generated@@137 $generated@@242) $generated@@243)) ))) -(assert (forall (($generated@@249 T@U) ($generated@@250 T@U) ($generated@@251 T@U) ($generated@@252 T@U) ($generated@@253 T@U) ($generated@@254 T@U) ($generated@@255 T@U) ($generated@@256 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@249 $generated@@250 $generated@@251 ($generated@@216 $generated@@252 $generated@@253 $generated@@254) $generated@@255) $generated@@256)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 ($generated@@42 $generated@@45 $generated@@23) $generated@@254 $generated@@251 $generated@@255) $generated@@256))) - :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@249 $generated@@250 $generated@@251 ($generated@@216 $generated@@252 $generated@@253 $generated@@254) $generated@@255) $generated@@256)) +(assert (forall (($generated@@245 T@U) ($generated@@246 T@U) ($generated@@247 T@U) ($generated@@248 T@U) ($generated@@249 T@U) ($generated@@250 T@U) ($generated@@251 T@U) ($generated@@252 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@245 $generated@@246 $generated@@247 ($generated@@212 $generated@@248 $generated@@249 $generated@@250) $generated@@251) $generated@@252)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 ($generated@@42 $generated@@45 $generated@@23) $generated@@250 $generated@@247 $generated@@251) $generated@@252))) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@245 $generated@@246 $generated@@247 ($generated@@212 $generated@@248 $generated@@249 $generated@@250) $generated@@251) $generated@@252)) ))) -(assert (forall (($generated@@257 T@U) ($generated@@258 T@U) ) (! (=> ($generated@@149 $generated@@257 $generated@@258) (= $generated@@257 $generated@@258)) - :pattern ( ($generated@@149 $generated@@257 $generated@@258)) +(assert (forall (($generated@@253 T@U) ($generated@@254 T@U) ) (! (=> ($generated@@149 $generated@@253 $generated@@254) (= $generated@@253 $generated@@254)) + :pattern ( ($generated@@149 $generated@@253 $generated@@254)) ))) -(assert (forall (($generated@@259 T@U) ($generated@@260 T@U) ($generated@@261 T@U) ) (! (=> (or (not (= $generated@@259 $generated@@261)) (not true)) (=> (and ($generated@@133 $generated@@259 $generated@@260) ($generated@@133 $generated@@260 $generated@@261)) ($generated@@133 $generated@@259 $generated@@261))) - :pattern ( ($generated@@133 $generated@@259 $generated@@260) ($generated@@133 $generated@@260 $generated@@261)) +(assert (forall (($generated@@255 T@U) ($generated@@256 T@U) ($generated@@257 T@U) ) (! (=> (or (not (= $generated@@255 $generated@@257)) (not true)) (=> (and ($generated@@133 $generated@@255 $generated@@256) ($generated@@133 $generated@@256 $generated@@257)) ($generated@@133 $generated@@255 $generated@@257))) + :pattern ( ($generated@@133 $generated@@255 $generated@@256) ($generated@@133 $generated@@256 $generated@@257)) ))) -(assert (forall (($generated@@262 T@U) ($generated@@263 T@U) ($generated@@264 T@U) ) (! (= ($generated@@98 $generated@@105 $generated@@262 ($generated@@106 $generated@@263 $generated@@264)) (forall (($generated@@265 T@U) ($generated@@266 T@U) ) (! (=> (and (and ($generated@@148 $generated@@265) ($generated@@47 $generated@@266 $generated@@263)) ($generated@@233 $generated@@263 $generated@@264 $generated@@265 $generated@@262 $generated@@266)) ($generated@@47 ($generated@@215 $generated@@263 $generated@@264 $generated@@265 $generated@@262 $generated@@266) $generated@@264)) - :pattern ( ($generated@@215 $generated@@263 $generated@@264 $generated@@265 $generated@@262 $generated@@266)) +(assert (forall (($generated@@258 T@U) ($generated@@259 T@U) ($generated@@260 T@U) ) (! (= ($generated@@98 $generated@@105 $generated@@258 ($generated@@106 $generated@@259 $generated@@260)) (forall (($generated@@261 T@U) ($generated@@262 T@U) ) (! (=> (and (and ($generated@@148 $generated@@261) ($generated@@47 $generated@@262 $generated@@259)) ($generated@@229 $generated@@259 $generated@@260 $generated@@261 $generated@@258 $generated@@262)) ($generated@@47 ($generated@@211 $generated@@259 $generated@@260 $generated@@261 $generated@@258 $generated@@262) $generated@@260)) + :pattern ( ($generated@@211 $generated@@259 $generated@@260 $generated@@261 $generated@@258 $generated@@262)) ))) - :pattern ( ($generated@@98 $generated@@105 $generated@@262 ($generated@@106 $generated@@263 $generated@@264))) + :pattern ( ($generated@@98 $generated@@105 $generated@@258 ($generated@@106 $generated@@259 $generated@@260))) ))) -(assert (forall (($generated@@268 T@U) ($generated@@269 T@U) ) (! (and (= ($generated@@267 ($generated@@122 $generated@@268 $generated@@269)) $generated@@268) (= ($generated@@40 ($generated@@122 $generated@@268 $generated@@269)) $generated@@269)) - :pattern ( ($generated@@122 $generated@@268 $generated@@269)) +(assert (forall (($generated@@264 T@U) ($generated@@265 T@U) ) (! (and (= ($generated@@263 ($generated@@122 $generated@@264 $generated@@265)) $generated@@264) (= ($generated@@40 ($generated@@122 $generated@@264 $generated@@265)) $generated@@265)) + :pattern ( ($generated@@122 $generated@@264 $generated@@265)) ))) -(assert (forall (($generated@@270 T@U) ($generated@@271 T@U) ($generated@@272 T@U) ($generated@@273 T@U) ) (! (=> ($generated@@148 $generated@@273) (= ($generated@@114 $generated@@105 $generated@@270 ($generated@@106 $generated@@271 $generated@@272) $generated@@273) (forall (($generated@@274 T@U) ) (! (=> (and (and ($generated@@47 $generated@@274 $generated@@271) ($generated@@186 $generated@@274 $generated@@271 $generated@@273)) ($generated@@233 $generated@@271 $generated@@272 $generated@@273 $generated@@270 $generated@@274)) (forall (($generated@@275 T@U) ) (! (=> (and (or (not (= $generated@@275 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@271 $generated@@272 $generated@@273 $generated@@270 $generated@@274) ($generated@@165 $generated@@43 $generated@@275)))) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@273 $generated@@275) $generated@@2)))) - :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@271 $generated@@272 $generated@@273 $generated@@270 $generated@@274) ($generated@@165 $generated@@43 $generated@@275))) +(assert (forall (($generated@@266 T@U) ($generated@@267 T@U) ($generated@@268 T@U) ($generated@@269 T@U) ) (! (=> ($generated@@148 $generated@@269) (= ($generated@@114 $generated@@105 $generated@@266 ($generated@@106 $generated@@267 $generated@@268) $generated@@269) (forall (($generated@@270 T@U) ) (! (=> (and (and ($generated@@47 $generated@@270 $generated@@267) ($generated@@182 $generated@@270 $generated@@267 $generated@@269)) ($generated@@229 $generated@@267 $generated@@268 $generated@@269 $generated@@266 $generated@@270)) (forall (($generated@@271 T@U) ) (! (=> (and (or (not (= $generated@@271 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@267 $generated@@268 $generated@@269 $generated@@266 $generated@@270) ($generated@@165 $generated@@43 $generated@@271)))) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@269 $generated@@271) $generated@@2)))) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@267 $generated@@268 $generated@@269 $generated@@266 $generated@@270) ($generated@@165 $generated@@43 $generated@@271))) ))) - :pattern ( ($generated@@215 $generated@@271 $generated@@272 $generated@@273 $generated@@270 $generated@@274)) - :pattern ( ($generated@@146 $generated@@271 $generated@@272 $generated@@273 $generated@@270 $generated@@274)) + :pattern ( ($generated@@211 $generated@@267 $generated@@268 $generated@@269 $generated@@266 $generated@@270)) + :pattern ( ($generated@@146 $generated@@267 $generated@@268 $generated@@269 $generated@@266 $generated@@270)) )))) - :pattern ( ($generated@@114 $generated@@105 $generated@@270 ($generated@@106 $generated@@271 $generated@@272) $generated@@273)) + :pattern ( ($generated@@114 $generated@@105 $generated@@266 ($generated@@106 $generated@@267 $generated@@268) $generated@@269)) ))) -(assert (forall (($generated@@276 T@U) ) (! (=> ($generated@@47 $generated@@276 $generated) (and (= ($generated@@165 $generated@@24 ($generated@@126 $generated@@24 $generated@@276)) $generated@@276) ($generated@@98 $generated@@24 ($generated@@126 $generated@@24 $generated@@276) $generated))) - :pattern ( ($generated@@47 $generated@@276 $generated)) +(assert (forall (($generated@@272 T@U) ) (! (=> ($generated@@47 $generated@@272 $generated) (and (= ($generated@@165 $generated@@24 ($generated@@126 $generated@@24 $generated@@272)) $generated@@272) ($generated@@98 $generated@@24 ($generated@@126 $generated@@24 $generated@@272) $generated))) + :pattern ( ($generated@@47 $generated@@272 $generated)) ))) -(assert (forall (($generated@@277 T@U) ($generated@@278 T@U) ($generated@@279 T@T) ) (! (= ($generated@@47 ($generated@@165 $generated@@279 $generated@@277) $generated@@278) ($generated@@98 $generated@@279 $generated@@277 $generated@@278)) - :pattern ( ($generated@@47 ($generated@@165 $generated@@279 $generated@@277) $generated@@278)) +(assert (forall (($generated@@273 T@U) ($generated@@274 T@U) ($generated@@275 T@T) ) (! (= ($generated@@47 ($generated@@165 $generated@@275 $generated@@273) $generated@@274) ($generated@@98 $generated@@275 $generated@@273 $generated@@274)) + :pattern ( ($generated@@47 ($generated@@165 $generated@@275 $generated@@273) $generated@@274)) ))) -(assert (forall (($generated@@280 T@U) ($generated@@281 T@U) ($generated@@282 T@U) ($generated@@283 T@U) ($generated@@284 T@U) ($generated@@285 T@U) ($generated@@286 T@U) ) (! (=> ($generated@@27 ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 $generated@@23 $generated@@284 $generated@@282 $generated@@286)) ($generated@@233 $generated@@280 $generated@@281 $generated@@282 ($generated@@216 $generated@@283 $generated@@284 $generated@@285) $generated@@286)) - :pattern ( ($generated@@233 $generated@@280 $generated@@281 $generated@@282 ($generated@@216 $generated@@283 $generated@@284 $generated@@285) $generated@@286)) +(assert (forall (($generated@@276 T@U) ($generated@@277 T@U) ($generated@@278 T@U) ($generated@@279 T@U) ($generated@@280 T@U) ($generated@@281 T@U) ($generated@@282 T@U) ) (! (=> ($generated@@27 ($generated@@41 ($generated@@42 $generated@@43 ($generated@@42 $generated@@44 $generated@@45)) $generated@@45 $generated@@23 $generated@@280 $generated@@278 $generated@@282)) ($generated@@229 $generated@@276 $generated@@277 $generated@@278 ($generated@@212 $generated@@279 $generated@@280 $generated@@281) $generated@@282)) + :pattern ( ($generated@@229 $generated@@276 $generated@@277 $generated@@278 ($generated@@212 $generated@@279 $generated@@280 $generated@@281) $generated@@282)) ))) -(assert (forall (($generated@@288 T@U) ($generated@@289 T@U) ) (! (= ($generated@@287 ($generated@@106 $generated@@288 $generated@@289)) $generated@@288) - :pattern ( ($generated@@106 $generated@@288 $generated@@289)) +(assert (forall (($generated@@284 T@U) ($generated@@285 T@U) ) (! (= ($generated@@283 ($generated@@106 $generated@@284 $generated@@285)) $generated@@284) + :pattern ( ($generated@@106 $generated@@284 $generated@@285)) ))) -(assert (forall (($generated@@291 T@U) ($generated@@292 T@U) ) (! (= ($generated@@290 ($generated@@106 $generated@@291 $generated@@292)) $generated@@292) - :pattern ( ($generated@@106 $generated@@291 $generated@@292)) +(assert (forall (($generated@@287 T@U) ($generated@@288 T@U) ) (! (= ($generated@@286 ($generated@@106 $generated@@287 $generated@@288)) $generated@@288) + :pattern ( ($generated@@106 $generated@@287 $generated@@288)) ))) -(assert (forall (($generated@@294 T@U) ($generated@@295 T@U) ) (! (= ($generated@@293 ($generated@@205 $generated@@294 $generated@@295)) $generated@@294) - :pattern ( ($generated@@205 $generated@@294 $generated@@295)) +(assert (forall (($generated@@290 T@U) ($generated@@291 T@U) ) (! (= ($generated@@289 ($generated@@201 $generated@@290 $generated@@291)) $generated@@290) + :pattern ( ($generated@@201 $generated@@290 $generated@@291)) ))) -(assert (forall (($generated@@297 T@U) ($generated@@298 T@U) ) (! (= ($generated@@296 ($generated@@205 $generated@@297 $generated@@298)) $generated@@298) - :pattern ( ($generated@@205 $generated@@297 $generated@@298)) +(assert (forall (($generated@@293 T@U) ($generated@@294 T@U) ) (! (= ($generated@@292 ($generated@@201 $generated@@293 $generated@@294)) $generated@@294) + :pattern ( ($generated@@201 $generated@@293 $generated@@294)) ))) -(assert (forall (($generated@@300 T@U) ($generated@@301 T@U) ) (! (= ($generated@@299 ($generated@@210 $generated@@300 $generated@@301)) $generated@@300) - :pattern ( ($generated@@210 $generated@@300 $generated@@301)) +(assert (forall (($generated@@296 T@U) ($generated@@297 T@U) ) (! (= ($generated@@295 ($generated@@206 $generated@@296 $generated@@297)) $generated@@296) + :pattern ( ($generated@@206 $generated@@296 $generated@@297)) ))) -(assert (forall (($generated@@303 T@U) ($generated@@304 T@U) ) (! (= ($generated@@302 ($generated@@210 $generated@@303 $generated@@304)) $generated@@304) - :pattern ( ($generated@@210 $generated@@303 $generated@@304)) +(assert (forall (($generated@@299 T@U) ($generated@@300 T@U) ) (! (= ($generated@@298 ($generated@@206 $generated@@299 $generated@@300)) $generated@@300) + :pattern ( ($generated@@206 $generated@@299 $generated@@300)) ))) -(assert (forall (($generated@@305 T@U) ) (! ($generated@@98 $generated@@43 $generated@@305 $generated@@125) - :pattern ( ($generated@@98 $generated@@43 $generated@@305 $generated@@125)) +(assert (forall (($generated@@301 T@U) ) (! ($generated@@98 $generated@@43 $generated@@301 $generated@@125) + :pattern ( ($generated@@98 $generated@@43 $generated@@301 $generated@@125)) ))) -(assert (forall (($generated@@307 T@U) ) (! (= ($generated@@306 ($generated@@137 $generated@@307)) $generated@@307) - :pattern ( ($generated@@137 $generated@@307)) +(assert (forall (($generated@@303 T@U) ) (! (= ($generated@@302 ($generated@@137 $generated@@303)) $generated@@303) + :pattern ( ($generated@@137 $generated@@303)) ))) -(assert (forall (($generated@@308 T@U) ) (! (= ($generated@@39 ($generated@@137 $generated@@308)) $generated@@1) - :pattern ( ($generated@@137 $generated@@308)) +(assert (forall (($generated@@304 T@U) ) (! (= ($generated@@39 ($generated@@137 $generated@@304)) $generated@@1) + :pattern ( ($generated@@137 $generated@@304)) ))) -(assert (forall (($generated@@309 T@U) ($generated@@310 T@T) ) (! (= ($generated@@126 $generated@@310 ($generated@@165 $generated@@310 $generated@@309)) $generated@@309) - :pattern ( ($generated@@165 $generated@@310 $generated@@309)) +(assert (forall (($generated@@305 T@U) ($generated@@306 T@T) ) (! (= ($generated@@126 $generated@@306 ($generated@@165 $generated@@306 $generated@@305)) $generated@@305) + :pattern ( ($generated@@165 $generated@@306 $generated@@305)) ))) -(assert (forall (($generated@@311 T@U) ($generated@@312 T@U) ) (! (=> (and ($generated@@148 $generated@@311) (and (or (not (= $generated@@312 $generated@@100)) (not true)) (= ($generated@@101 $generated@@312) $generated@@103))) ($generated@@98 $generated@@24 ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@311 $generated@@312) $generated@@124)) $generated)) - :pattern ( ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@311 $generated@@312) $generated@@124))) +(assert (forall (($generated@@307 T@U) ($generated@@308 T@U) ) (! (=> (and ($generated@@148 $generated@@307) (and (or (not (= $generated@@308 $generated@@100)) (not true)) (= ($generated@@101 $generated@@308) $generated@@103))) ($generated@@98 $generated@@24 ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@307 $generated@@308) $generated@@124)) $generated)) + :pattern ( ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@307 $generated@@308) $generated@@124))) ))) -(assert (forall (($generated@@313 T@U) ($generated@@314 T@U) ($generated@@315 T@U) ) (! (= ($generated@@98 $generated@@105 $generated@@315 ($generated@@210 $generated@@313 $generated@@314)) (and ($generated@@98 $generated@@105 $generated@@315 ($generated@@205 $generated@@313 $generated@@314)) (forall (($generated@@316 T@U) ) (=> ($generated@@47 $generated@@316 $generated@@313) ($generated@@233 $generated@@313 $generated@@314 $generated@@147 $generated@@315 $generated@@316))))) - :pattern ( ($generated@@98 $generated@@105 $generated@@315 ($generated@@210 $generated@@313 $generated@@314))) +(assert (forall (($generated@@309 T@U) ($generated@@310 T@U) ($generated@@311 T@U) ) (! (= ($generated@@98 $generated@@105 $generated@@311 ($generated@@206 $generated@@309 $generated@@310)) (and ($generated@@98 $generated@@105 $generated@@311 ($generated@@201 $generated@@309 $generated@@310)) (forall (($generated@@312 T@U) ) (=> ($generated@@47 $generated@@312 $generated@@309) ($generated@@229 $generated@@309 $generated@@310 $generated@@147 $generated@@311 $generated@@312))))) + :pattern ( ($generated@@98 $generated@@105 $generated@@311 ($generated@@206 $generated@@309 $generated@@310))) ))) -(assert (forall (($generated@@317 T@U) ($generated@@318 T@U) ($generated@@319 T@U) ) (! (= ($generated@@98 $generated@@105 $generated@@319 ($generated@@205 $generated@@317 $generated@@318)) (and ($generated@@98 $generated@@105 $generated@@319 ($generated@@106 $generated@@317 $generated@@318)) (forall (($generated@@320 T@U) ) (=> ($generated@@47 $generated@@320 $generated@@317) ($generated@@149 ($generated@@146 $generated@@317 $generated@@318 $generated@@147 $generated@@319 $generated@@320) $generated@@150))))) - :pattern ( ($generated@@98 $generated@@105 $generated@@319 ($generated@@205 $generated@@317 $generated@@318))) +(assert (forall (($generated@@313 T@U) ($generated@@314 T@U) ($generated@@315 T@U) ) (! (= ($generated@@98 $generated@@105 $generated@@315 ($generated@@201 $generated@@313 $generated@@314)) (and ($generated@@98 $generated@@105 $generated@@315 ($generated@@106 $generated@@313 $generated@@314)) (forall (($generated@@316 T@U) ) (=> ($generated@@47 $generated@@316 $generated@@313) ($generated@@149 ($generated@@146 $generated@@313 $generated@@314 $generated@@147 $generated@@315 $generated@@316) $generated@@150))))) + :pattern ( ($generated@@98 $generated@@105 $generated@@315 ($generated@@201 $generated@@313 $generated@@314))) ))) -(assert (forall (($generated@@322 T@U) ($generated@@323 T@U) ($generated@@324 T@T) ) (! (= ($generated@@179 $generated@@324 $generated@@322 ($generated@@321 $generated@@323)) ($generated@@179 $generated@@324 $generated@@322 $generated@@323)) - :pattern ( ($generated@@179 $generated@@324 $generated@@322 ($generated@@321 $generated@@323))) +(assert (forall (($generated@@318 T@U) ($generated@@319 T@U) ($generated@@320 T@T) ) (! (= ($generated@@175 $generated@@320 $generated@@318 ($generated@@317 $generated@@319)) ($generated@@175 $generated@@320 $generated@@318 $generated@@319)) + :pattern ( ($generated@@175 $generated@@320 $generated@@318 ($generated@@317 $generated@@319))) ))) -(assert (forall (($generated@@325 T@U) ($generated@@326 T@U) ($generated@@327 T@U) ) (! (=> ($generated@@47 $generated@@327 ($generated@@106 $generated@@325 $generated@@326)) (and (= ($generated@@165 $generated@@105 ($generated@@126 $generated@@105 $generated@@327)) $generated@@327) ($generated@@98 $generated@@105 ($generated@@126 $generated@@105 $generated@@327) ($generated@@106 $generated@@325 $generated@@326)))) - :pattern ( ($generated@@47 $generated@@327 ($generated@@106 $generated@@325 $generated@@326))) +(assert (forall (($generated@@321 T@U) ($generated@@322 T@U) ($generated@@323 T@U) ) (! (=> ($generated@@47 $generated@@323 ($generated@@106 $generated@@321 $generated@@322)) (and (= ($generated@@165 $generated@@105 ($generated@@126 $generated@@105 $generated@@323)) $generated@@323) ($generated@@98 $generated@@105 ($generated@@126 $generated@@105 $generated@@323) ($generated@@106 $generated@@321 $generated@@322)))) + :pattern ( ($generated@@47 $generated@@323 ($generated@@106 $generated@@321 $generated@@322))) ))) -(assert (forall (($generated@@328 T@U) ($generated@@329 T@U) ($generated@@330 T@U) ) (! (=> ($generated@@47 $generated@@330 ($generated@@205 $generated@@328 $generated@@329)) (and (= ($generated@@165 $generated@@105 ($generated@@126 $generated@@105 $generated@@330)) $generated@@330) ($generated@@98 $generated@@105 ($generated@@126 $generated@@105 $generated@@330) ($generated@@205 $generated@@328 $generated@@329)))) - :pattern ( ($generated@@47 $generated@@330 ($generated@@205 $generated@@328 $generated@@329))) +(assert (forall (($generated@@324 T@U) ($generated@@325 T@U) ($generated@@326 T@U) ) (! (=> ($generated@@47 $generated@@326 ($generated@@201 $generated@@324 $generated@@325)) (and (= ($generated@@165 $generated@@105 ($generated@@126 $generated@@105 $generated@@326)) $generated@@326) ($generated@@98 $generated@@105 ($generated@@126 $generated@@105 $generated@@326) ($generated@@201 $generated@@324 $generated@@325)))) + :pattern ( ($generated@@47 $generated@@326 ($generated@@201 $generated@@324 $generated@@325))) ))) -(assert (forall (($generated@@331 T@U) ($generated@@332 T@U) ($generated@@333 T@U) ) (! (=> ($generated@@47 $generated@@333 ($generated@@210 $generated@@331 $generated@@332)) (and (= ($generated@@165 $generated@@105 ($generated@@126 $generated@@105 $generated@@333)) $generated@@333) ($generated@@98 $generated@@105 ($generated@@126 $generated@@105 $generated@@333) ($generated@@210 $generated@@331 $generated@@332)))) - :pattern ( ($generated@@47 $generated@@333 ($generated@@210 $generated@@331 $generated@@332))) +(assert (forall (($generated@@327 T@U) ($generated@@328 T@U) ($generated@@329 T@U) ) (! (=> ($generated@@47 $generated@@329 ($generated@@206 $generated@@327 $generated@@328)) (and (= ($generated@@165 $generated@@105 ($generated@@126 $generated@@105 $generated@@329)) $generated@@329) ($generated@@98 $generated@@105 ($generated@@126 $generated@@105 $generated@@329) ($generated@@206 $generated@@327 $generated@@328)))) + :pattern ( ($generated@@47 $generated@@329 ($generated@@206 $generated@@327 $generated@@328))) ))) +(assert (=> (<= 1 $generated@@330) (forall (($generated@@331 T@U) ($generated@@332 Int) ($generated@@333 T@U) ) (! (=> (or ($generated@@158 $generated@@331 $generated@@332 $generated@@333) (and (< 1 $generated@@330) (and ($generated@@148 $generated@@331) (and ($generated@@98 $generated@@43 $generated@@333 $generated@@115) ($generated@@114 $generated@@43 $generated@@333 $generated@@115 $generated@@331))))) (and (= ($generated@@157 $generated@@331 $generated@@332 $generated@@333) ($generated@@29 ($generated@@126 $generated@@24 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@331 ($generated@@126 $generated@@43 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@331 $generated@@333) $generated@@121))) $generated@@124)))) (<= ($generated@@141 0) ($generated@@157 $generated@@331 $generated@@332 $generated@@333)))) + :pattern ( ($generated@@157 $generated@@331 $generated@@332 $generated@@333)) +)))) (assert (forall (($generated@@334 T@U) ) (! (not ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@150 $generated@@334))) :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@150 $generated@@334)) ))) @@ -921,15 +921,15 @@ $generated@@192)))))) (assert (forall (($generated@@343 T@U) ($generated@@344 T@U) ) (! (and (= ($generated@@39 ($generated@@106 $generated@@343 $generated@@344)) $generated@@5) (= ($generated@@342 ($generated@@106 $generated@@343 $generated@@344)) $generated@@15)) :pattern ( ($generated@@106 $generated@@343 $generated@@344)) ))) -(assert (forall (($generated@@345 T@U) ($generated@@346 T@U) ) (! (and (= ($generated@@39 ($generated@@205 $generated@@345 $generated@@346)) $generated@@6) (= ($generated@@342 ($generated@@205 $generated@@345 $generated@@346)) $generated@@16)) - :pattern ( ($generated@@205 $generated@@345 $generated@@346)) +(assert (forall (($generated@@345 T@U) ($generated@@346 T@U) ) (! (and (= ($generated@@39 ($generated@@201 $generated@@345 $generated@@346)) $generated@@6) (= ($generated@@342 ($generated@@201 $generated@@345 $generated@@346)) $generated@@16)) + :pattern ( ($generated@@201 $generated@@345 $generated@@346)) ))) -(assert (forall (($generated@@347 T@U) ($generated@@348 T@U) ) (! (and (= ($generated@@39 ($generated@@210 $generated@@347 $generated@@348)) $generated@@7) (= ($generated@@342 ($generated@@210 $generated@@347 $generated@@348)) $generated@@17)) - :pattern ( ($generated@@210 $generated@@347 $generated@@348)) +(assert (forall (($generated@@347 T@U) ($generated@@348 T@U) ) (! (and (= ($generated@@39 ($generated@@206 $generated@@347 $generated@@348)) $generated@@7) (= ($generated@@342 ($generated@@206 $generated@@347 $generated@@348)) $generated@@17)) + :pattern ( ($generated@@206 $generated@@347 $generated@@348)) ))) -(assert (forall (($generated@@349 T@U) ($generated@@350 T@U) ($generated@@351 T@U) ($generated@@352 T@U) ($generated@@353 T@U) ) (! (=> (and (and ($generated@@148 $generated@@351) (and ($generated@@47 $generated@@353 $generated@@349) ($generated@@98 $generated@@105 $generated@@352 ($generated@@106 $generated@@349 $generated@@350)))) ($generated@@149 ($generated@@146 $generated@@349 $generated@@350 $generated@@147 $generated@@352 $generated@@353) $generated@@150)) (= ($generated@@233 $generated@@349 $generated@@350 $generated@@147 $generated@@352 $generated@@353) ($generated@@233 $generated@@349 $generated@@350 $generated@@351 $generated@@352 $generated@@353))) - :pattern ( ($generated@@233 $generated@@349 $generated@@350 $generated@@147 $generated@@352 $generated@@353) ($generated@@148 $generated@@351)) - :pattern ( ($generated@@233 $generated@@349 $generated@@350 $generated@@351 $generated@@352 $generated@@353)) +(assert (forall (($generated@@349 T@U) ($generated@@350 T@U) ($generated@@351 T@U) ($generated@@352 T@U) ($generated@@353 T@U) ) (! (=> (and (and ($generated@@148 $generated@@351) (and ($generated@@47 $generated@@353 $generated@@349) ($generated@@98 $generated@@105 $generated@@352 ($generated@@106 $generated@@349 $generated@@350)))) ($generated@@149 ($generated@@146 $generated@@349 $generated@@350 $generated@@147 $generated@@352 $generated@@353) $generated@@150)) (= ($generated@@229 $generated@@349 $generated@@350 $generated@@147 $generated@@352 $generated@@353) ($generated@@229 $generated@@349 $generated@@350 $generated@@351 $generated@@352 $generated@@353))) + :pattern ( ($generated@@229 $generated@@349 $generated@@350 $generated@@147 $generated@@352 $generated@@353) ($generated@@148 $generated@@351)) + :pattern ( ($generated@@229 $generated@@349 $generated@@350 $generated@@351 $generated@@352 $generated@@353)) ))) (assert (forall (($generated@@354 T@U) ($generated@@355 T@U) ) (! (=> ($generated@@47 $generated@@354 ($generated@@137 $generated@@355)) (and (= ($generated@@165 ($generated@@42 $generated@@45 $generated@@23) ($generated@@126 ($generated@@42 $generated@@45 $generated@@23) $generated@@354)) $generated@@354) ($generated@@98 ($generated@@42 $generated@@45 $generated@@23) ($generated@@126 ($generated@@42 $generated@@45 $generated@@23) $generated@@354) ($generated@@137 $generated@@355)))) :pattern ( ($generated@@47 $generated@@354 ($generated@@137 $generated@@355))) @@ -944,14 +944,14 @@ $generated@@192)))))) (assert (= ($generated@@342 $generated@@118) $generated@@19)) (assert (= ($generated@@39 $generated@@103) $generated@@13)) (assert (= ($generated@@342 $generated@@103) $generated@@19)) -(assert (forall (($generated@@356 T@U) ) (! ($generated@@98 ($generated@@42 $generated@@45 $generated@@23) ($generated@@176 $generated@@356) ($generated@@137 $generated@@125)) - :pattern ( ($generated@@176 $generated@@356)) +(assert (forall (($generated@@356 T@U) ) (! ($generated@@98 ($generated@@42 $generated@@45 $generated@@23) ($generated@@172 $generated@@356) ($generated@@137 $generated@@125)) + :pattern ( ($generated@@172 $generated@@356)) ))) -(assert (forall (($generated@@357 T@U) ($generated@@358 T@U) ($generated@@359 T@U) ($generated@@360 T@U) ($generated@@361 T@U) ($generated@@362 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@359 $generated@@360) (and ($generated@@148 $generated@@359) ($generated@@148 $generated@@360))) (and ($generated@@47 $generated@@362 $generated@@357) ($generated@@98 $generated@@105 $generated@@361 ($generated@@106 $generated@@357 $generated@@358)))) (forall (($generated@@363 T@U) ($generated@@364 T@U) ) (=> (and (or (not (= $generated@@363 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@357 $generated@@358 $generated@@359 $generated@@361 $generated@@362) ($generated@@165 $generated@@43 $generated@@363)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@359 $generated@@363) $generated@@364) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@360 $generated@@363) $generated@@364))))) (= ($generated@@233 $generated@@357 $generated@@358 $generated@@359 $generated@@361 $generated@@362) ($generated@@233 $generated@@357 $generated@@358 $generated@@360 $generated@@361 $generated@@362))) - :pattern ( ($generated@@133 $generated@@359 $generated@@360) ($generated@@233 $generated@@357 $generated@@358 $generated@@360 $generated@@361 $generated@@362)) +(assert (forall (($generated@@357 T@U) ($generated@@358 T@U) ($generated@@359 T@U) ($generated@@360 T@U) ($generated@@361 T@U) ($generated@@362 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@359 $generated@@360) (and ($generated@@148 $generated@@359) ($generated@@148 $generated@@360))) (and ($generated@@47 $generated@@362 $generated@@357) ($generated@@98 $generated@@105 $generated@@361 ($generated@@106 $generated@@357 $generated@@358)))) (forall (($generated@@363 T@U) ($generated@@364 T@U) ) (=> (and (or (not (= $generated@@363 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@357 $generated@@358 $generated@@359 $generated@@361 $generated@@362) ($generated@@165 $generated@@43 $generated@@363)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@359 $generated@@363) $generated@@364) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@360 $generated@@363) $generated@@364))))) (= ($generated@@229 $generated@@357 $generated@@358 $generated@@359 $generated@@361 $generated@@362) ($generated@@229 $generated@@357 $generated@@358 $generated@@360 $generated@@361 $generated@@362))) + :pattern ( ($generated@@133 $generated@@359 $generated@@360) ($generated@@229 $generated@@357 $generated@@358 $generated@@360 $generated@@361 $generated@@362)) ))) -(assert (forall (($generated@@365 T@U) ($generated@@366 T@U) ($generated@@367 T@U) ($generated@@368 T@U) ($generated@@369 T@U) ($generated@@370 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@367 $generated@@368) (and ($generated@@148 $generated@@367) ($generated@@148 $generated@@368))) (and ($generated@@47 $generated@@370 $generated@@365) ($generated@@98 $generated@@105 $generated@@369 ($generated@@106 $generated@@365 $generated@@366)))) (forall (($generated@@371 T@U) ($generated@@372 T@U) ) (=> (and (or (not (= $generated@@371 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@365 $generated@@366 $generated@@368 $generated@@369 $generated@@370) ($generated@@165 $generated@@43 $generated@@371)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@367 $generated@@371) $generated@@372) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@368 $generated@@371) $generated@@372))))) (= ($generated@@233 $generated@@365 $generated@@366 $generated@@367 $generated@@369 $generated@@370) ($generated@@233 $generated@@365 $generated@@366 $generated@@368 $generated@@369 $generated@@370))) - :pattern ( ($generated@@133 $generated@@367 $generated@@368) ($generated@@233 $generated@@365 $generated@@366 $generated@@368 $generated@@369 $generated@@370)) +(assert (forall (($generated@@365 T@U) ($generated@@366 T@U) ($generated@@367 T@U) ($generated@@368 T@U) ($generated@@369 T@U) ($generated@@370 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@367 $generated@@368) (and ($generated@@148 $generated@@367) ($generated@@148 $generated@@368))) (and ($generated@@47 $generated@@370 $generated@@365) ($generated@@98 $generated@@105 $generated@@369 ($generated@@106 $generated@@365 $generated@@366)))) (forall (($generated@@371 T@U) ($generated@@372 T@U) ) (=> (and (or (not (= $generated@@371 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@365 $generated@@366 $generated@@368 $generated@@369 $generated@@370) ($generated@@165 $generated@@43 $generated@@371)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@367 $generated@@371) $generated@@372) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@368 $generated@@371) $generated@@372))))) (= ($generated@@229 $generated@@365 $generated@@366 $generated@@367 $generated@@369 $generated@@370) ($generated@@229 $generated@@365 $generated@@366 $generated@@368 $generated@@369 $generated@@370))) + :pattern ( ($generated@@133 $generated@@367 $generated@@368) ($generated@@229 $generated@@365 $generated@@366 $generated@@368 $generated@@369 $generated@@370)) ))) (assert (forall (($generated@@373 Int) ) (! (= ($generated@@165 $generated@@24 ($generated@@28 ($generated@@141 $generated@@373))) ($generated@@143 $generated@@45 ($generated@@165 $generated@@24 ($generated@@28 $generated@@373)))) :pattern ( ($generated@@165 $generated@@24 ($generated@@28 ($generated@@141 $generated@@373)))) @@ -965,13 +965,13 @@ $generated@@192)))))) (assert (forall (($generated@@384 T@U) ($generated@@385 T@U) ($generated@@386 T@U) ($generated@@387 T@U) ($generated@@388 T@U) ($generated@@389 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@386 $generated@@387) (and ($generated@@148 $generated@@386) ($generated@@148 $generated@@387))) (and ($generated@@47 $generated@@389 $generated@@384) ($generated@@98 $generated@@105 $generated@@388 ($generated@@106 $generated@@384 $generated@@385)))) (forall (($generated@@390 T@U) ($generated@@391 T@U) ) (=> (and (or (not (= $generated@@390 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@384 $generated@@385 $generated@@387 $generated@@388 $generated@@389) ($generated@@165 $generated@@43 $generated@@390)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@386 $generated@@390) $generated@@391) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@387 $generated@@390) $generated@@391))))) (= ($generated@@146 $generated@@384 $generated@@385 $generated@@386 $generated@@388 $generated@@389) ($generated@@146 $generated@@384 $generated@@385 $generated@@387 $generated@@388 $generated@@389))) :pattern ( ($generated@@133 $generated@@386 $generated@@387) ($generated@@146 $generated@@384 $generated@@385 $generated@@387 $generated@@388 $generated@@389)) ))) -(assert (forall (($generated@@392 T@U) ($generated@@393 T@U) ($generated@@394 T@U) ($generated@@395 T@U) ($generated@@396 T@U) ($generated@@397 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@394 $generated@@395) (and ($generated@@148 $generated@@394) ($generated@@148 $generated@@395))) (and ($generated@@47 $generated@@397 $generated@@392) ($generated@@98 $generated@@105 $generated@@396 ($generated@@106 $generated@@392 $generated@@393)))) (forall (($generated@@398 T@U) ($generated@@399 T@U) ) (=> (and (or (not (= $generated@@398 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@392 $generated@@393 $generated@@394 $generated@@396 $generated@@397) ($generated@@165 $generated@@43 $generated@@398)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@394 $generated@@398) $generated@@399) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@395 $generated@@398) $generated@@399))))) (= ($generated@@215 $generated@@392 $generated@@393 $generated@@394 $generated@@396 $generated@@397) ($generated@@215 $generated@@392 $generated@@393 $generated@@395 $generated@@396 $generated@@397))) - :pattern ( ($generated@@133 $generated@@394 $generated@@395) ($generated@@215 $generated@@392 $generated@@393 $generated@@395 $generated@@396 $generated@@397)) +(assert (forall (($generated@@392 T@U) ($generated@@393 T@U) ($generated@@394 T@U) ($generated@@395 T@U) ($generated@@396 T@U) ($generated@@397 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@394 $generated@@395) (and ($generated@@148 $generated@@394) ($generated@@148 $generated@@395))) (and ($generated@@47 $generated@@397 $generated@@392) ($generated@@98 $generated@@105 $generated@@396 ($generated@@106 $generated@@392 $generated@@393)))) (forall (($generated@@398 T@U) ($generated@@399 T@U) ) (=> (and (or (not (= $generated@@398 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@392 $generated@@393 $generated@@394 $generated@@396 $generated@@397) ($generated@@165 $generated@@43 $generated@@398)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@394 $generated@@398) $generated@@399) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@395 $generated@@398) $generated@@399))))) (= ($generated@@211 $generated@@392 $generated@@393 $generated@@394 $generated@@396 $generated@@397) ($generated@@211 $generated@@392 $generated@@393 $generated@@395 $generated@@396 $generated@@397))) + :pattern ( ($generated@@133 $generated@@394 $generated@@395) ($generated@@211 $generated@@392 $generated@@393 $generated@@395 $generated@@396 $generated@@397)) ))) -(assert (forall (($generated@@400 T@U) ($generated@@401 T@U) ($generated@@402 T@U) ($generated@@403 T@U) ($generated@@404 T@U) ($generated@@405 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@402 $generated@@403) (and ($generated@@148 $generated@@402) ($generated@@148 $generated@@403))) (and ($generated@@47 $generated@@405 $generated@@400) ($generated@@98 $generated@@105 $generated@@404 ($generated@@106 $generated@@400 $generated@@401)))) (forall (($generated@@406 T@U) ($generated@@407 T@U) ) (=> (and (or (not (= $generated@@406 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@400 $generated@@401 $generated@@403 $generated@@404 $generated@@405) ($generated@@165 $generated@@43 $generated@@406)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@402 $generated@@406) $generated@@407) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@403 $generated@@406) $generated@@407))))) (= ($generated@@215 $generated@@400 $generated@@401 $generated@@402 $generated@@404 $generated@@405) ($generated@@215 $generated@@400 $generated@@401 $generated@@403 $generated@@404 $generated@@405))) - :pattern ( ($generated@@133 $generated@@402 $generated@@403) ($generated@@215 $generated@@400 $generated@@401 $generated@@403 $generated@@404 $generated@@405)) +(assert (forall (($generated@@400 T@U) ($generated@@401 T@U) ($generated@@402 T@U) ($generated@@403 T@U) ($generated@@404 T@U) ($generated@@405 T@U) ) (! (=> (and (and (and ($generated@@133 $generated@@402 $generated@@403) (and ($generated@@148 $generated@@402) ($generated@@148 $generated@@403))) (and ($generated@@47 $generated@@405 $generated@@400) ($generated@@98 $generated@@105 $generated@@404 ($generated@@106 $generated@@400 $generated@@401)))) (forall (($generated@@406 T@U) ($generated@@407 T@U) ) (=> (and (or (not (= $generated@@406 $generated@@100)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@146 $generated@@400 $generated@@401 $generated@@403 $generated@@404 $generated@@405) ($generated@@165 $generated@@43 $generated@@406)))) (= ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@402 $generated@@406) $generated@@407) ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@403 $generated@@406) $generated@@407))))) (= ($generated@@211 $generated@@400 $generated@@401 $generated@@402 $generated@@404 $generated@@405) ($generated@@211 $generated@@400 $generated@@401 $generated@@403 $generated@@404 $generated@@405))) + :pattern ( ($generated@@133 $generated@@402 $generated@@403) ($generated@@211 $generated@@400 $generated@@401 $generated@@403 $generated@@404 $generated@@405)) ))) -(assert (=> (<= 1 $generated@@168) (forall (($generated@@408 T@U) ($generated@@409 Int) ($generated@@410 T@U) ) (! (=> (or ($generated@@158 $generated@@408 $generated@@409 $generated@@410) (and (< 1 $generated@@168) (and ($generated@@148 $generated@@408) ($generated@@98 $generated@@43 $generated@@410 $generated@@115)))) (= ($generated@@157 $generated@@408 $generated@@409 $generated@@410) ($generated@@141 3))) +(assert (=> (<= 1 $generated@@330) (forall (($generated@@408 T@U) ($generated@@409 Int) ($generated@@410 T@U) ) (! (=> (or ($generated@@158 $generated@@408 $generated@@409 $generated@@410) (and (< 1 $generated@@330) (and ($generated@@148 $generated@@408) ($generated@@98 $generated@@43 $generated@@410 $generated@@115)))) (= ($generated@@157 $generated@@408 $generated@@409 $generated@@410) ($generated@@141 3))) :pattern ( ($generated@@157 $generated@@408 $generated@@409 $generated@@410) ($generated@@148 $generated@@408)) )))) (assert (forall (($generated@@411 T@U) ($generated@@412 T@U) ) (! ($generated@@114 $generated@@24 $generated@@412 $generated $generated@@411) @@ -1020,13 +1020,13 @@ $generated@@192)))))) (let (($generated@@435 true)) (let (($generated@@436 (=> (and ($generated@@148 $generated@@418) (or (= $generated@@419 $generated@@418) ($generated@@133 $generated@@419 $generated@@418))) (and (=> (= (ControlFlow 0 7) 5) $generated@@435) (=> (= (ControlFlow 0 7) 6) $generated@@434))))) (let (($generated@@437 (=> (= (ControlFlow 0 2) (- 0 1)) (= $generated@@420 (= $generated@@421 ($generated@@141 2)))))) -(let (($generated@@438 (=> (= $generated@@422 ($generated@@143 $generated@@105 ($generated@@179 $generated@@105 ($generated@@242 ($generated@@216 ($generated@@172 1) ($generated@@46 $generated) ($generated@@413 ($generated@@176 ($generated@@239 false))))) ($generated@@321 $generated@@423)))) (=> (and (and (or (not (= $generated@@424 $generated@@100)) (not true)) (and ($generated@@98 $generated@@43 $generated@@424 $generated@@115) ($generated@@114 $generated@@43 $generated@@424 $generated@@115 $generated@@425))) (and ($generated@@148 $generated@@426) ($generated@@156 $generated@@426))) (=> (and (and (and (or (not (= $generated@@427 $generated@@100)) (not true)) (and ($generated@@98 $generated@@43 $generated@@427 $generated@@115) ($generated@@114 $generated@@43 $generated@@427 $generated@@115 $generated@@426))) (not ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@419 $generated@@427) $generated@@2))))) (and (forall (($generated@@439 T@U) ) (! (=> (and (or (not (= $generated@@439 $generated@@100)) (not true)) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@419 $generated@@439) $generated@@2)))) (= ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@426 $generated@@439) ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@419 $generated@@439))) +(let (($generated@@438 (=> (= $generated@@422 ($generated@@143 $generated@@105 ($generated@@175 $generated@@105 ($generated@@238 ($generated@@212 ($generated@@168 1) ($generated@@46 $generated) ($generated@@413 ($generated@@172 ($generated@@235 false))))) ($generated@@317 $generated@@423)))) (=> (and (and (or (not (= $generated@@424 $generated@@100)) (not true)) (and ($generated@@98 $generated@@43 $generated@@424 $generated@@115) ($generated@@114 $generated@@43 $generated@@424 $generated@@115 $generated@@425))) (and ($generated@@148 $generated@@426) ($generated@@156 $generated@@426))) (=> (and (and (and (or (not (= $generated@@427 $generated@@100)) (not true)) (and ($generated@@98 $generated@@43 $generated@@427 $generated@@115) ($generated@@114 $generated@@43 $generated@@427 $generated@@115 $generated@@426))) (not ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@419 $generated@@427) $generated@@2))))) (and (forall (($generated@@439 T@U) ) (! (=> (and (or (not (= $generated@@439 $generated@@100)) (not true)) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@419 $generated@@439) $generated@@2)))) (= ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@426 $generated@@439) ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@419 $generated@@439))) :pattern ( ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@426 $generated@@439)) )) ($generated@@133 $generated@@419 $generated@@426))) (and (=> (= (ControlFlow 0 3) (- 0 4)) true) (=> (and (and (and (= $generated@@428 ($generated@@141 42)) ($generated@@114 $generated@@24 ($generated@@28 $generated@@428) $generated $generated@@426)) (and ($generated@@114 $generated@@43 $generated@@427 $generated@@115 $generated@@426) ($generated@@158 $generated@@426 ($generated@@141 42) $generated@@427))) (and (and ($generated@@158 $generated@@426 ($generated@@141 42) $generated@@427) (= $generated@@429 (= $generated@@421 ($generated@@157 $generated@@426 ($generated@@141 42) $generated@@427)))) (and (= $generated@@420 $generated@@429) (= (ControlFlow 0 3) 2)))) $generated@@437))))))) (let (($generated@@440 (=> (= $generated@@430 ($generated@@335 $generated@@100 $generated@@425 $generated@@2 false)) (=> (and (and (and ($generated@@148 $generated@@419) ($generated@@156 $generated@@419)) ($generated@@27 ($generated@@143 $generated@@23 ($generated@@26 false)))) (and (forall (($generated@@441 T@U) ) (! (=> (and (or (not (= $generated@@441 $generated@@100)) (not true)) ($generated@@27 ($generated@@126 $generated@@23 ($generated@@49 $generated@@44 $generated@@45 ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@425 $generated@@441) $generated@@2)))) (= ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@419 $generated@@441) ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@425 $generated@@441))) :pattern ( ($generated@@49 $generated@@43 ($generated@@42 $generated@@44 $generated@@45) $generated@@419 $generated@@441)) )) ($generated@@133 $generated@@425 $generated@@419))) (and (=> (= (ControlFlow 0 8) 7) $generated@@436) (=> (= (ControlFlow 0 8) 3) $generated@@438)))))) -(let (($generated@@442 (=> (and ($generated@@148 $generated@@425) ($generated@@156 $generated@@425)) (=> (and (and ($generated@@98 $generated@@105 $generated@@431 ($generated@@210 $generated $generated)) ($generated@@114 $generated@@105 $generated@@431 ($generated@@210 $generated $generated) $generated@@425)) true) (=> (and (and (and (=> $generated@@432 (and ($generated@@98 $generated@@43 $generated@@433 $generated@@115) ($generated@@114 $generated@@43 $generated@@433 $generated@@115 $generated@@425))) true) (= 2 $generated@@168)) (and (= $generated@@421 ($generated@@141 2)) (= (ControlFlow 0 9) 8))) $generated@@440))))) +(let (($generated@@442 (=> (and ($generated@@148 $generated@@425) ($generated@@156 $generated@@425)) (=> (and (and ($generated@@98 $generated@@105 $generated@@431 ($generated@@206 $generated $generated)) ($generated@@114 $generated@@105 $generated@@431 ($generated@@206 $generated $generated) $generated@@425)) true) (=> (and (and (and (=> $generated@@432 (and ($generated@@98 $generated@@43 $generated@@433 $generated@@115) ($generated@@114 $generated@@43 $generated@@433 $generated@@115 $generated@@425))) true) (= 2 $generated@@330)) (and (= $generated@@421 ($generated@@141 2)) (= (ControlFlow 0 9) 8))) $generated@@440))))) $generated@@442)))))))) )) (check-sat) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect index faa2edf577c..ca00b3beab3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect @@ -1,6 +1,6 @@ DefaultParameters.dfy(55,23): Error: default-value expression is not allowed to involve recursive or mutually recursive calls -DefaultParameters.dfy(63,42): Error: default value might not be allocated in the two-state function's previous state -DefaultParameters.dfy(67,38): Error: default value might not be allocated in the two-state lemma's previous state +DefaultParameters.dfy(63,42): Error: default value could not be proved to be allocated in the two-state function's previous state +DefaultParameters.dfy(67,38): Error: default value could not be proved to be allocated in the two-state lemma's previous state DefaultParameters.dfy(92,2): Error: a postcondition could not be proved on this return path DefaultParameters.dfy(91,16): Related location: this is the postcondition that could not be proved DefaultParameters.dfy(102,15): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabelsOldAt.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabelsOldAt.dfy.expect index f06ea587233..0f5a0aa2708 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabelsOldAt.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabelsOldAt.dfy.expect @@ -10,28 +10,28 @@ LabelsOldAt.dfy(116,13): Error: assertion might not hold LabelsOldAt.dfy(118,13): Error: assertion might not hold LabelsOldAt.dfy(140,13): Error: assertion might not hold LabelsOldAt.dfy(142,13): Error: assertion might not hold -LabelsOldAt.dfy(164,21): Error: receiver might not be allocated in the state in which its fields are accessed -LabelsOldAt.dfy(166,27): Error: receiver might not be allocated in the state in which its fields are accessed -LabelsOldAt.dfy(175,19): Error: array might not be allocated -LabelsOldAt.dfy(177,25): Error: array might not be allocated -LabelsOldAt.dfy(195,25): Error: object might not be allocated in the old-state of the 'unchanged' predicate -LabelsOldAt.dfy(197,31): Error: object might not be allocated in the old-state of the 'unchanged' predicate -LabelsOldAt.dfy(207,31): Error: some set element might not be allocated in the old-state of the 'unchanged' predicate -LabelsOldAt.dfy(236,14): Error: receiver might not be allocated in the state in which its fields are accessed -LabelsOldAt.dfy(244,29): Error: object might not be allocated in the old-state of the 'unchanged' predicate -LabelsOldAt.dfy(246,29): Error: some set element might not be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(164,21): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +LabelsOldAt.dfy(166,27): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +LabelsOldAt.dfy(175,19): Error: array could not be proved to be allocated +LabelsOldAt.dfy(177,25): Error: array could not be proved to be allocated +LabelsOldAt.dfy(195,25): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(197,31): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(207,31): Error: some set element could not be proved to be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(236,14): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +LabelsOldAt.dfy(244,29): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(246,29): Error: some set element could not be proved to be allocated in the old-state of the 'unchanged' predicate LabelsOldAt.dfy(266,15): Error: object might be null LabelsOldAt.dfy(267,15): Error: some set element might be null LabelsOldAt.dfy(268,15): Error: some sequence element might be null -LabelsOldAt.dfy(274,15): Error: object might not be allocated in the old-state of the 'unchanged' predicate -LabelsOldAt.dfy(275,15): Error: some set element might not be allocated in the old-state of the 'unchanged' predicate -LabelsOldAt.dfy(276,15): Error: some sequence element might not be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(274,15): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(275,15): Error: some set element could not be proved to be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(276,15): Error: some sequence element could not be proved to be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(281,15): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate LabelsOldAt.dfy(281,15): Error: object might be null -LabelsOldAt.dfy(281,15): Error: object might not be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(286,15): Error: some set element could not be proved to be allocated in the old-state of the 'unchanged' predicate LabelsOldAt.dfy(286,15): Error: some set element might be null -LabelsOldAt.dfy(286,15): Error: some set element might not be allocated in the old-state of the 'unchanged' predicate +LabelsOldAt.dfy(291,15): Error: some sequence element could not be proved to be allocated in the old-state of the 'unchanged' predicate LabelsOldAt.dfy(291,15): Error: some sequence element might be null -LabelsOldAt.dfy(291,15): Error: some sequence element might not be allocated in the old-state of the 'unchanged' predicate LabelsOldAt.dfy(358,11): Error: assertion might not hold LabelsOldAt.dfy(367,11): Error: assertion might not hold LabelsOldAt.dfy(376,11): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Functions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Functions.dfy.expect index fc00f04fb91..a7aced49240 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Functions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Functions.dfy.expect @@ -1,17 +1,17 @@ -Twostate-Functions.dfy(11,27): Error: receiver might not be allocated in the state in which its fields are accessed -Twostate-Functions.dfy(18,12): Error: receiver might not be allocated in the state in which its fields are accessed +Twostate-Functions.dfy(11,27): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +Twostate-Functions.dfy(18,12): Error: receiver could not be proved to be allocated in the state in which its fields are accessed Twostate-Functions.dfy(23,8): Error: insufficient reads clause to read field Twostate-Functions.dfy(66,17): Error: assertion might not hold Twostate-Functions.dfy(54,14): Related location: this proposition could not be proved Twostate-Functions.dfy(68,15): Error: assertion might not hold Twostate-Functions.dfy(54,14): Related location: this proposition could not be proved -Twostate-Functions.dfy(92,24): Error: argument ('u') might not be allocated in the two-state function's previous state -Twostate-Functions.dfy(97,40): Error: argument at index 1 ('x') might not be allocated in the two-state function's previous state -Twostate-Functions.dfy(129,25): Error: receiver might not be allocated in the state in which its fields are accessed -Twostate-Functions.dfy(147,12): Error: receiver might not be allocated in the state in which its fields are accessed -Twostate-Functions.dfy(164,15): Error: argument ('d') might not be allocated in the two-state function's previous state +Twostate-Functions.dfy(92,24): Error: argument for parameter 'u' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new u: U', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Functions.dfy(97,40): Error: argument at index 1 for parameter 'x' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new x: U', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Functions.dfy(129,25): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +Twostate-Functions.dfy(147,12): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +Twostate-Functions.dfy(164,15): Error: argument for parameter 'd' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new d: D', arguments can refer to expressions possibly unallocated in the previous state Twostate-Functions.dfy(167,13): Error: function precondition could not be proved -Twostate-Functions.dfy(183,15): Error: argument ('d') might not be allocated in the two-state function's previous state +Twostate-Functions.dfy(183,15): Error: argument for parameter 'd' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new d: D', arguments can refer to expressions possibly unallocated in the previous state Twostate-Functions.dfy(186,13): Error: function precondition could not be proved Dafny program verifier finished with 25 verified, 13 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect index 9d39631ff1e..6e44d6b5033 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect @@ -26,45 +26,45 @@ Twostate-Verification.dfy(337,23): Error: a precondition for this call could not Twostate-Verification.dfy(317,29): Related location: this is the precondition that could not be proved Twostate-Verification.dfy(359,18): Error: assertion might not hold Twostate-Verification.dfy(361,18): Error: assertion might not hold -Twostate-Verification.dfy(384,17): Error: receiver argument might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(386,17): Error: receiver argument might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(391,26): Error: argument at index 0 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(393,28): Error: argument at index 0 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(398,19): Error: receiver argument might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(412,8): Error: receiver argument might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(414,8): Error: receiver argument might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(420,27): Error: parameter at index 0 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(422,29): Error: parameter at index 0 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(447,28): Error: argument at index 0 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(451,30): Error: argument at index 0 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(466,29): Error: parameter at index 0 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(470,31): Error: parameter at index 0 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(558,22): Error: argument at index 2 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(561,22): Error: parameter at index 2 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(564,22): Error: argument at index 2 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(567,22): Error: parameter at index 2 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(579,11): Error: receiver argument might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(582,11): Error: receiver argument might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(593,19): Error: argument at index 1 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(596,19): Error: parameter at index 1 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(599,19): Error: argument at index 1 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(602,19): Error: parameter at index 1 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(613,22): Error: argument at index 2 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(616,22): Error: parameter at index 2 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(619,26): Error: argument at index 3 ('c') might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(622,26): Error: parameter at index 3 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(635,25): Error: receiver argument might not be allocated in the two-state function's previous state -Twostate-Verification.dfy(659,29): Error: receiver might not be allocated in the state in which its fields are accessed +Twostate-Verification.dfy(384,17): Error: receiver argument could not be proved to be allocated in the two-state function's previous state +Twostate-Verification.dfy(386,17): Error: receiver argument could not be proved to be allocated in the two-state function's previous state +Twostate-Verification.dfy(391,26): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(393,28): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(398,19): Error: receiver argument could not be proved to be allocated in the two-state function's previous state +Twostate-Verification.dfy(412,8): Error: receiver argument could not be proved to be allocated in the two-state lemma's previous state +Twostate-Verification.dfy(414,8): Error: receiver argument could not be proved to be allocated in the two-state lemma's previous state +Twostate-Verification.dfy(420,27): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(422,29): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(447,28): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(451,30): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(466,29): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(470,31): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(558,22): Error: argument at index 2 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(561,22): Error: argument at index 2 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(564,22): Error: argument at index 2 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(567,22): Error: argument at index 2 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(579,11): Error: receiver argument could not be proved to be allocated in the two-state function's previous state +Twostate-Verification.dfy(582,11): Error: receiver argument could not be proved to be allocated in the two-state lemma's previous state +Twostate-Verification.dfy(593,19): Error: argument at index 1 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(596,19): Error: argument at index 1 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(599,19): Error: argument at index 1 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(602,19): Error: argument at index 1 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(613,22): Error: argument at index 2 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(616,22): Error: argument at index 2 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(619,26): Error: argument at index 3 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(622,26): Error: argument at index 3 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(635,25): Error: receiver argument could not be proved to be allocated in the two-state function's previous state +Twostate-Verification.dfy(659,29): Error: receiver could not be proved to be allocated in the state in which its fields are accessed Twostate-Verification.dfy(271,13): Error: a postcondition could not be proved on this return path Twostate-Verification.dfy(263,24): Related location: this is the postcondition that could not be proved Twostate-Verification.dfy(277,4): Error: a postcondition could not be proved on this return path Twostate-Verification.dfy(276,26): Related location: this is the postcondition that could not be proved -Twostate-Verification.dfy(6,4): Error: parameter at index 0 ('c') might not be allocated in the two-state lemma's previous state -Twostate-Verification.dfy(12,17): Error: receiver might not be allocated in the state in which its fields are accessed -Twostate-Verification.dfy(37,26): Error: receiver might not be allocated in the state in which its fields are accessed -Twostate-Verification.dfy(41,32): Error: receiver argument might not be allocated in the state in which the function is invoked -Twostate-Verification.dfy(56,26): Error: receiver might not be allocated in the state in which its fields are accessed -Twostate-Verification.dfy(58,32): Error: receiver argument might not be allocated in the state in which the function is invoked +Twostate-Verification.dfy(6,4): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new c: A', arguments can refer to expressions possibly unallocated in the previous state +Twostate-Verification.dfy(12,17): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +Twostate-Verification.dfy(37,26): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +Twostate-Verification.dfy(41,32): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked +Twostate-Verification.dfy(56,26): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +Twostate-Verification.dfy(58,32): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked Twostate-Verification.dfy(74,15): Error: assertion might not hold Dafny program verifier finished with 66 verified, 42 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Unchanged.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Unchanged.dfy.expect index f4f44c1e0c6..3ed7c60cfb7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Unchanged.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Unchanged.dfy.expect @@ -2,9 +2,9 @@ Unchanged.dfy(33,25): Error: assertion might not hold Unchanged.dfy(34,25): Error: assertion might not hold Unchanged.dfy(35,25): Error: assertion might not hold Unchanged.dfy(38,13): Error: assertion might not hold -Unchanged.dfy(46,35): Error: object might not be allocated in the old-state of the 'unchanged' predicate -Unchanged.dfy(47,35): Error: object might not be allocated in the old-state of the 'unchanged' predicate -Unchanged.dfy(48,41): Error: object might not be allocated in the old-state of the 'unchanged' predicate -Unchanged.dfy(49,35): Error: object might not be allocated in the old-state of the 'unchanged' predicate +Unchanged.dfy(46,35): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate +Unchanged.dfy(47,35): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate +Unchanged.dfy(48,41): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate +Unchanged.dfy(49,35): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate Dafny program verifier finished with 1 verified, 8 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug132.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug132.dfy.expect index 22055966205..652411be7ed 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug132.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug132.dfy.expect @@ -1,6 +1,6 @@ -Bug132.dfy(33,29): Error: receiver argument might not be allocated in the state in which the function is invoked -Bug132.dfy(34,29): Error: receiver argument might not be allocated in the state in which the function is invoked -Bug132.dfy(37,36): Error: argument might not be allocated in the state in which the function is invoked -Bug132.dfy(41,29): Error: receiver argument might not be allocated in the state in which the function is invoked +Bug132.dfy(33,29): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked +Bug132.dfy(34,29): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked +Bug132.dfy(37,36): Error: argument could not be proved to be allocated in the state in which the function is invoked +Bug132.dfy(41,29): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked Dafny program verifier finished with 2 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue51.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue51.dfy.expect index 1af66232088..91c80279a79 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue51.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue51.dfy.expect @@ -1,12 +1,12 @@ -git-issue51.dfy(35,15): Error: argument might not be allocated in the state in which the function is invoked -git-issue51.dfy(38,20): Error: argument might not be allocated in the state in which the function is invoked -git-issue51.dfy(42,15): Error: argument might not be allocated in the state in which the method is invoked -git-issue51.dfy(45,15): Error: argument might not be allocated in the state in which the method is invoked -git-issue51.dfy(53,22): Error: argument might not be allocated in the state in which the function is invoked -git-issue51.dfy(57,19): Error: argument might not be allocated in the state in which the method is invoked -git-issue51.dfy(59,17): Error: argument might not be allocated in the state in which the function is invoked -git-issue51.dfy(69,12): Error: parameter at index 0 ('a') might not be allocated in the two-state lemma's previous state -git-issue51.dfy(75,15): Error: receiver might not be allocated in the state in which its fields are accessed -git-issue51.dfy(79,11): Error: argument at index 0 ('a') might not be allocated in the two-state function's previous state +git-issue51.dfy(35,15): Error: argument could not be proved to be allocated in the state in which the function is invoked +git-issue51.dfy(38,20): Error: argument could not be proved to be allocated in the state in which the function is invoked +git-issue51.dfy(42,15): Error: argument could not be proved to be allocated in the state in which the method is invoked +git-issue51.dfy(45,15): Error: argument could not be proved to be allocated in the state in which the method is invoked +git-issue51.dfy(53,22): Error: argument could not be proved to be allocated in the state in which the function is invoked +git-issue51.dfy(57,19): Error: argument could not be proved to be allocated in the state in which the method is invoked +git-issue51.dfy(59,17): Error: argument could not be proved to be allocated in the state in which the function is invoked +git-issue51.dfy(69,12): Error: argument at index 0 for parameter 'a' could not be proved to be allocated in the two-state lemma's previous state -- if you add 'new' before the parameter declaration, like 'new a: C', arguments can refer to expressions possibly unallocated in the previous state +git-issue51.dfy(75,15): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +git-issue51.dfy(79,11): Error: argument at index 0 for parameter 'a' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new a: C', arguments can refer to expressions possibly unallocated in the previous state Dafny program verifier finished with 2 verified, 10 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1112.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1112.dfy.expect index 080f08a4e12..61e95c65f03 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1112.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1112.dfy.expect @@ -7,12 +7,12 @@ git-issue-1112.dfy(38,44): Error: target object might be null git-issue-1112.dfy(51,33): Error: target object might be null git-issue-1112.dfy(53,25): Error: target object might be null git-issue-1112.dfy(53,46): Error: target object might be null -git-issue-1112.dfy(64,26): Error: receiver might not be allocated in the state in which its fields are accessed -git-issue-1112.dfy(66,28): Error: receiver might not be allocated in the state in which its fields are accessed -git-issue-1112.dfy(77,23): Error: array might not be allocated -git-issue-1112.dfy(79,25): Error: array might not be allocated -git-issue-1112.dfy(90,23): Error: array might not be allocated -git-issue-1112.dfy(92,25): Error: array might not be allocated +git-issue-1112.dfy(64,26): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +git-issue-1112.dfy(66,28): Error: receiver could not be proved to be allocated in the state in which its fields are accessed +git-issue-1112.dfy(77,23): Error: array could not be proved to be allocated +git-issue-1112.dfy(79,25): Error: array could not be proved to be allocated +git-issue-1112.dfy(90,23): Error: array could not be proved to be allocated +git-issue-1112.dfy(92,25): Error: array could not be proved to be allocated git-issue-1112.dfy(98,11): Error: array might be null git-issue-1112.dfy(98,14): Error: index out of range git-issue-1112.dfy(99,11): Error: array might be null diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1163.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1163.dfy.expect index 3f619a04c07..fd7de1ef0d2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1163.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1163.dfy.expect @@ -1,6 +1,6 @@ git-issue-1163.dfy(7,17): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect -git-issue-1163.dfy(21,42): Error: receiver argument might not be allocated in the state in which the function is invoked -git-issue-1163.dfy(23,44): Error: argument might not be allocated in the state in which the function is invoked -git-issue-1163.dfy(27,40): Error: receiver argument might not be allocated in the state in which the function is invoked +git-issue-1163.dfy(21,42): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked +git-issue-1163.dfy(23,44): Error: argument could not be proved to be allocated in the state in which the function is invoked +git-issue-1163.dfy(27,40): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked Dafny program verifier finished with 2 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1252.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1252.dfy.expect index 7d00bd734ae..e3b1f4d26dd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1252.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1252.dfy.expect @@ -12,8 +12,8 @@ git-issue-1252.dfy(93,13): Error: target object might be null git-issue-1252.dfy(94,10): Error: target object might be null git-issue-1252.dfy(94,10): Error: target object might be null git-issue-1252.dfy(100,25): Error: target object might be null +git-issue-1252.dfy(106,21): Error: object could not be proved to be allocated in the old-state of the 'unchanged' predicate git-issue-1252.dfy(106,21): Error: object might be null -git-issue-1252.dfy(106,21): Error: object might not be allocated in the old-state of the 'unchanged' predicate git-issue-1252.dfy(106,21): Error: target object might be null Dafny program verifier finished with 4 verified, 16 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect index 802b5ada1dc..2bb07b70a75 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect @@ -10,10 +10,10 @@ git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,4): Related location: this proposition could not be proved git-issue-2299.dfy(10,11): Related location: this proposition could not be proved git-issue-2299.dfy(81,11): Error: assertion might not hold -git-issue-2299.dfy(27,32): Related location: this proposition could not be proved -git-issue-2299.dfy(21,4): Related location: this proposition could not be proved -git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,18): Related location: this proposition could not be proved git-issue-2299.dfy(16,4): Related location: this proposition could not be proved +git-issue-2299.dfy(81,11): Error: assertion might not hold +git-issue-2299.dfy(27,32): Related location: this proposition could not be proved +git-issue-2299.dfy(21,4): Related location: this proposition could not be proved Dafny program verifier finished with 7 verified, 7 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4844.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4844.dfy new file mode 100644 index 00000000000..06b1803f44b --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4844.dfy @@ -0,0 +1,18 @@ +// RUN: %exits-with 4 %baredafny verify %args "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Ooops() + ensures false +{ + var x := new O(); + assert AllocationSoundness(x); +} + +class O { + var x: int + constructor() {} +} + +twostate predicate AllocationSoundness(o: O) + ensures old(allocated(o)) +{ true } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4844.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4844.dfy.expect new file mode 100644 index 00000000000..042916a5d6a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4844.dfy.expect @@ -0,0 +1,3 @@ +git-issue-4844.dfy(8,29): Error: argument for parameter 'o' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new o: O', arguments can refer to expressions possibly unallocated in the previous state + +Dafny program verifier finished with 1 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect index 9de0165d0e5..1be7ec6e5d8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect @@ -1,6 +1,6 @@ -Apply.dfy(46,23): Error: function might not be allocated in the state in which the function is invoked -Apply.dfy(57,31): Error: argument might not be allocated in the state in which the function is invoked -Apply.dfy(58,31): Error: argument might not be allocated in the state in which the function is invoked -Apply.dfy(61,31): Error: argument might not be allocated in the state in which the function is invoked +Apply.dfy(46,23): Error: function could not be proved to be allocated in the state in which the function is invoked +Apply.dfy(57,31): Error: argument could not be proved to be allocated in the state in which the function is invoked +Apply.dfy(58,31): Error: argument could not be proved to be allocated in the state in which the function is invoked +Apply.dfy(61,31): Error: argument could not be proved to be allocated in the state in which the function is invoked Dafny program verifier finished with 4 verified, 4 errors diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index ed3efdb6b92..fbc0f868936 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -32,7 +32,7 @@ public static ILitCommand Parse(string[] args) { public static string? Run(string expectedOutputFile, string actualOutput) { if (UpdateExpectFile) { - var path = Path.GetFullPath(expectedOutputFile).Replace("bin/Debug/net6.0/", ""); + var path = Path.GetFullPath(expectedOutputFile).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, ""); File.WriteAllText(path, actualOutput); return null; } diff --git a/docs/DafnyRef/Types.11.expect b/docs/DafnyRef/Types.11.expect index 607b134067d..881c05e2302 100644 --- a/docs/DafnyRef/Types.11.expect +++ b/docs/DafnyRef/Types.11.expect @@ -1,3 +1,3 @@ -text.dfy(11,25): Error: argument at index 1 ('d') might not be allocated in the two-state function's previous state +text.dfy(11,25): Error: argument at index 1 for parameter 'd' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new d: Cell', arguments can refer to expressions possibly unallocated in the previous state Dafny program verifier finished with 2 verified, 1 error diff --git a/docs/DafnyRef/Types.12.expect b/docs/DafnyRef/Types.12.expect index 92111995947..ef354a07b10 100644 --- a/docs/DafnyRef/Types.12.expect +++ b/docs/DafnyRef/Types.12.expect @@ -1,3 +1,3 @@ -text.dfy(10,27): Error: argument at index 0 ('c') might not be allocated in the two-state function's previous state +text.dfy(10,27): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state Dafny program verifier finished with 2 verified, 1 error diff --git a/docs/dev/news/4844.fix b/docs/dev/news/4844.fix new file mode 100644 index 00000000000..29dc060bae6 --- /dev/null +++ b/docs/dev/news/4844.fix @@ -0,0 +1 @@ +(soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap \ No newline at end of file