tribuchet: building on jamie > [1/3] Checking whether the inductive invariant 'indInv' holds in the initial state(s) defined by 'init'... # Usage statistics is OFF. We care about your privacy. # If you want to help our project, consider enabling statistics with config --enable-stats=true. Output directory: /build/_apalache-out/server/2026-10-25T16-54-06_9433390518880753966 # APALACHE version: 0.62.1 | build: a321771 I@16:54:06.710 Starting checker server on port 8822... I@16:54:06.714 The Apalache server is running on port 8822. Press Ctrl-C to stop. Failed to find a usable hardware address from the network interfaces; using random bytes: b3:c5:af:d6:fe:fe:24:16 W@16:54:07.484 Oct 25, 2026 4:54:10 PM com.google.protobuf.GeneratedMessage warnPre22Gencode WARNING: Vulnerable protobuf generated type in use: io.grpc.reflection.v1alpha.ServerReflectionRequest As of 2022/09/29 (release 21.7) makeExtensionsImmutable should not be called from protobuf gencode. If you are seeing this message, your gencode is vulnerable to a denial of service attack. You should regenerate your code using protobuf 25.6 or later. Use the latest version that meets your needs. However, if you understand the risks and wish to continue with vulnerable gencode, you can set the system property `-Dcom.google.protobuf.use_unsafe_pre22_gencode` on the command line to silence this warning. You also can set `-Dcom.google.protobuf.error_on_unsafe_pre22_gencode` to throw an error instead. See security vulnerability: https://github.com/protocolbuffers/protobuf/security/advisories/GHSA-h4h5-3hr4-j3g2 PASS #0: SanyParser I@16:54:10.901 PASS #1: TypeCheckerSnowcat I@16:54:11.626 > Running Snowcat .::. I@16:54:11.626 > Your types are purrfect! I@16:54:13.885 > All expressions are typed I@16:54:13.886 PASS #2: ConfigurationPass I@16:54:13.887 > Set the initialization predicate to q::init I@16:54:13.892 > Set the transition predicate to q::step I@16:54:13.892 > Set an invariant to q::inductiveInv I@16:54:13.892 PASS #3: DesugarerPass I@16:54:13.899 > Desugaring... I@16:54:13.900 PASS #4: InlinePass I@16:54:13.915 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:13.915 PASS #5: TemporalPass I@16:54:14.019 > Rewriting temporal operators... I@16:54:14.019 > No temporal property specified, nothing to encode I@16:54:14.019 PASS #6: InlinePass I@16:54:14.019 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:14.019 PASS #7: PrimingPass I@16:54:14.045 > Introducing q::initPrimed for q::init' I@16:54:14.048 PASS #8: VCGen I@16:54:14.049 > Producing verification conditions from the invariant q::inductiveInv I@16:54:14.049 > VCGen produced 39 verification condition(s) I@16:54:14.058 PASS #9: PreprocessingPass I@16:54:14.064 > Before preprocessing: unique renaming I@16:54:14.064 > Applying standard transformations: I@16:54:14.072 > PrimePropagation I@16:54:14.072 > Desugarer I@16:54:14.080 > UniqueRenamer I@16:54:14.088 > Normalizer I@16:54:14.115 > SetMembershipSimplifier I@16:54:14.135 > Keramelizer I@16:54:14.145 > After preprocessing: UniqueRenamer I@16:54:14.168 PASS #10: TransitionFinderPass I@16:54:14.211 > Found 1 initializing transitions I@16:54:14.225 > Found 24 transitions I@16:54:14.259 > No constant initializer I@16:54:14.259 > Applying unique renaming I@16:54:14.261 PASS #11: OptimizationPass I@16:54:14.289 > Applying optimizations: I@16:54:14.294 > ConstSimplifier I@16:54:14.294 > ExprOptimizer I@16:54:14.366 > SetMembershipSimplifier I@16:54:14.390 > ConstSimplifier I@16:54:14.397 PASS #12: AnalysisPass I@16:54:14.468 > Marking skolemizable existentials and sets to be expanded... I@16:54:14.471 > Skolemization I@16:54:14.471 > Expansion I@16:54:14.476 > Remove unused let-in defs I@16:54:14.495 > Running analyzers... I@16:54:14.507 > Introduced expression grades I@16:54:14.517 PASS #13: BoundedChecker I@16:54:14.517 State 0: Checking 39 state invariants I@16:54:15.007 State 0: state invariant 0 holds. I@16:54:15.014 State 0: state invariant 1 holds. I@16:54:15.068 State 0: state invariant 2 holds. I@16:54:15.069 State 0: state invariant 3 holds. I@16:54:15.070 State 0: state invariant 4 holds. I@16:54:15.109 State 0: state invariant 5 holds. I@16:54:15.114 State 0: state invariant 6 holds. I@16:54:15.116 State 0: state invariant 7 holds. I@16:54:15.117 State 0: state invariant 8 holds. I@16:54:15.118 State 0: state invariant 9 holds. I@16:54:15.126 State 0: state invariant 10 holds. I@16:54:15.127 State 0: state invariant 11 holds. I@16:54:15.127 State 0: state invariant 12 holds. I@16:54:15.137 State 0: state invariant 13 holds. I@16:54:15.138 State 0: state invariant 14 holds. I@16:54:15.146 State 0: state invariant 15 holds. I@16:54:15.147 State 0: state invariant 16 holds. I@16:54:15.148 State 0: state invariant 17 holds. I@16:54:15.148 State 0: state invariant 18 holds. I@16:54:15.151 State 0: state invariant 19 holds. I@16:54:15.156 State 0: state invariant 20 holds. I@16:54:15.166 State 0: state invariant 21 holds. I@16:54:15.175 State 0: state invariant 22 holds. I@16:54:15.180 State 0: state invariant 23 holds. I@16:54:15.191 State 0: state invariant 24 holds. I@16:54:15.195 State 0: state invariant 25 holds. I@16:54:15.196 State 0: state invariant 26 holds. I@16:54:15.202 State 0: state invariant 27 holds. I@16:54:15.214 State 0: state invariant 28 holds. I@16:54:15.233 State 0: state invariant 29 holds. I@16:54:15.241 State 0: state invariant 30 holds. I@16:54:15.263 State 0: state invariant 31 holds. I@16:54:15.299 State 0: state invariant 32 holds. I@16:54:15.328 State 0: state invariant 33 holds. I@16:54:15.329 State 0: state invariant 34 holds. I@16:54:15.334 State 0: state invariant 35 holds. I@16:54:15.339 State 0: state invariant 36 holds. I@16:54:15.341 State 0: state invariant 37 holds. I@16:54:15.342 State 0: state invariant 38 holds. I@16:54:15.342 Step 0: picking a transition out of 1 transition(s) I@16:54:15.343 The outcome is: NoError I@16:54:15.351 > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... PASS #0: SanyParser I@16:54:15.670 PASS #1: TypeCheckerSnowcat I@16:54:15.824 > Running Snowcat .::. I@16:54:15.824 > Your types are purrfect! I@16:54:18.418 > All expressions are typed I@16:54:18.419 PASS #2: ConfigurationPass I@16:54:18.419 > Set the initialization predicate to q::inductiveInv I@16:54:18.419 > Set the transition predicate to q::step I@16:54:18.420 > Set an invariant to q::inductiveInv I@16:54:18.420 PASS #3: DesugarerPass I@16:54:18.422 > Desugaring... I@16:54:18.422 PASS #4: InlinePass I@16:54:18.424 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:18.424 PASS #5: TemporalPass I@16:54:18.454 > Rewriting temporal operators... I@16:54:18.454 > No temporal property specified, nothing to encode I@16:54:18.454 PASS #6: InlinePass I@16:54:18.455 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:18.455 PASS #7: PrimingPass I@16:54:18.465 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:18.465 PASS #8: VCGen I@16:54:18.466 > Producing verification conditions from the invariant q::inductiveInv I@16:54:18.466 > VCGen produced 39 verification condition(s) I@16:54:18.467 PASS #9: PreprocessingPass I@16:54:18.469 > Before preprocessing: unique renaming I@16:54:18.469 > Applying standard transformations: I@16:54:18.469 > PrimePropagation I@16:54:18.470 > Desugarer I@16:54:18.472 > UniqueRenamer I@16:54:18.476 > Normalizer I@16:54:18.487 > SetMembershipSimplifier I@16:54:18.503 > Keramelizer I@16:54:18.506 > After preprocessing: UniqueRenamer I@16:54:18.516 PASS #10: TransitionFinderPass I@16:54:18.530 > Found 1 initializing transitions I@16:54:18.533 > Found 24 transitions I@16:54:18.543 > No constant initializer I@16:54:18.543 > Applying unique renaming I@16:54:18.544 PASS #11: OptimizationPass I@16:54:18.566 > Applying optimizations: I@16:54:18.566 > ConstSimplifier I@16:54:18.566 > ExprOptimizer I@16:54:18.648 > SetMembershipSimplifier I@16:54:18.661 > ConstSimplifier I@16:54:18.665 PASS #12: AnalysisPass I@16:54:18.739 > Marking skolemizable existentials and sets to be expanded... I@16:54:18.739 > Skolemization I@16:54:18.739 > Expansion I@16:54:18.743 > Remove unused let-in defs I@16:54:18.756 > Running analyzers... I@16:54:18.760 > Introduced expression grades I@16:54:18.762 PASS #13: BoundedChecker I@16:54:18.762 State 0: Checking 39 state invariants I@16:54:19.497 State 0: state invariant 0 holds. I@16:54:19.503 State 0: state invariant 1 holds. I@16:54:19.531 State 0: state invariant 2 holds. I@16:54:19.535 State 0: state invariant 3 holds. I@16:54:19.537 State 0: state invariant 4 holds. I@16:54:19.563 State 0: state invariant 5 holds. I@16:54:19.574 State 0: state invariant 6 holds. I@16:54:19.577 State 0: state invariant 7 holds. I@16:54:19.578 State 0: state invariant 8 holds. I@16:54:19.579 State 0: state invariant 9 holds. I@16:54:19.581 State 0: state invariant 10 holds. I@16:54:19.582 State 0: state invariant 11 holds. I@16:54:19.584 State 0: state invariant 12 holds. I@16:54:19.591 State 0: state invariant 13 holds. I@16:54:19.594 State 0: state invariant 14 holds. I@16:54:19.603 State 0: state invariant 15 holds. I@16:54:19.605 State 0: state invariant 16 holds. I@16:54:19.606 State 0: state invariant 17 holds. I@16:54:19.607 State 0: state invariant 18 holds. I@16:54:19.614 State 0: state invariant 19 holds. I@16:54:19.620 State 0: state invariant 20 holds. I@16:54:19.628 State 0: state invariant 21 holds. I@16:54:19.642 State 0: state invariant 22 holds. I@16:54:19.652 State 0: state invariant 23 holds. I@16:54:19.662 State 0: state invariant 24 holds. I@16:54:19.663 State 0: state invariant 25 holds. I@16:54:19.664 State 0: state invariant 26 holds. I@16:54:19.666 State 0: state invariant 27 holds. I@16:54:19.672 State 0: state invariant 28 holds. I@16:54:19.697 State 0: state invariant 29 holds. I@16:54:19.706 State 0: state invariant 30 holds. I@16:54:19.835 State 0: state invariant 31 holds. I@16:54:19.976 State 0: state invariant 32 holds. I@16:54:20.129 State 0: state invariant 33 holds. I@16:54:20.132 State 0: state invariant 34 holds. I@16:54:20.138 State 0: state invariant 35 holds. I@16:54:20.144 State 0: state invariant 36 holds. I@16:54:20.145 State 0: state invariant 37 holds. I@16:54:20.146 State 0: state invariant 38 holds. I@16:54:20.147 Step 0: picking a transition out of 1 transition(s) I@16:54:20.148 State 1: Checking 12 state invariants I@16:54:20.176 State 1: state invariant 0 holds. I@16:54:20.178 State 1: state invariant 1 holds. I@16:54:20.210 State 1: state invariant 18 holds. I@16:54:20.220 State 1: state invariant 19 holds. I@16:54:20.227 State 1: state invariant 20 holds. I@16:54:20.236 State 1: state invariant 21 holds. I@16:54:20.247 State 1: state invariant 27 holds. I@16:54:20.258 State 1: state invariant 28 holds. I@16:54:20.287 State 1: state invariant 29 holds. I@16:54:20.296 State 1: state invariant 30 holds. I@16:54:20.428 State 1: state invariant 31 holds. I@16:54:20.562 State 1: state invariant 32 holds. I@16:54:20.663 State 1: Checking 4 state invariants I@16:54:20.686 State 1: state invariant 13 holds. I@16:54:20.688 State 1: state invariant 29 holds. I@16:54:20.694 State 1: state invariant 30 holds. I@16:54:20.818 State 1: state invariant 31 holds. I@16:54:20.949 State 1: Checking 16 state invariants I@16:54:21.002 State 1: state invariant 0 holds. I@16:54:21.003 State 1: state invariant 1 holds. I@16:54:21.027 State 1: state invariant 3 holds. I@16:54:21.030 State 1: state invariant 4 holds. I@16:54:21.053 State 1: state invariant 5 holds. I@16:54:21.062 State 1: state invariant 18 holds. I@16:54:21.069 State 1: state invariant 19 holds. I@16:54:21.075 State 1: state invariant 20 holds. I@16:54:21.082 State 1: state invariant 21 holds. I@16:54:21.090 State 1: state invariant 23 holds. I@16:54:21.100 State 1: state invariant 27 holds. I@16:54:21.105 State 1: state invariant 28 holds. I@16:54:21.124 State 1: state invariant 29 holds. I@16:54:21.132 State 1: state invariant 30 holds. I@16:54:21.232 State 1: state invariant 31 holds. I@16:54:21.345 State 1: state invariant 32 holds. I@16:54:21.436 State 1: Checking 6 state invariants I@16:54:21.455 State 1: state invariant 2 holds. I@16:54:21.457 State 1: state invariant 27 holds. I@16:54:21.473 State 1: state invariant 29 holds. I@16:54:21.480 State 1: state invariant 30 holds. I@16:54:21.729 State 1: state invariant 31 holds. I@16:54:21.888 State 1: state invariant 38 holds. I@16:54:21.892 State 1: Checking 15 state invariants I@16:54:21.910 State 1: state invariant 0 holds. I@16:54:21.911 State 1: state invariant 1 holds. I@16:54:21.937 State 1: state invariant 2 holds. I@16:54:21.939 State 1: state invariant 12 holds. I@16:54:21.948 State 1: state invariant 18 holds. I@16:54:21.956 State 1: state invariant 19 holds. I@16:54:21.965 State 1: state invariant 20 holds. I@16:54:21.973 State 1: state invariant 21 holds. I@16:54:21.983 State 1: state invariant 27 holds. I@16:54:21.992 State 1: state invariant 28 holds. I@16:54:22.027 State 1: state invariant 29 holds. I@16:54:22.036 State 1: state invariant 30 holds. I@16:54:22.187 State 1: state invariant 31 holds. I@16:54:22.326 State 1: state invariant 32 holds. I@16:54:22.474 State 1: state invariant 37 holds. I@16:54:22.477 State 1: Checking 18 state invariants I@16:54:22.693 State 1: state invariant 9 holds. I@16:54:22.698 State 1: state invariant 10 holds. I@16:54:22.699 State 1: state invariant 11 holds. I@16:54:22.700 State 1: state invariant 14 holds. I@16:54:22.708 State 1: state invariant 15 holds. I@16:54:22.710 State 1: state invariant 17 holds. I@16:54:22.711 State 1: state invariant 22 holds. I@16:54:22.719 State 1: state invariant 24 holds. I@16:54:22.721 State 1: state invariant 26 holds. I@16:54:22.723 State 1: state invariant 27 holds. I@16:54:22.731 State 1: state invariant 28 holds. I@16:54:22.753 State 1: state invariant 29 holds. I@16:54:22.760 State 1: state invariant 30 holds. I@16:54:22.816 State 1: state invariant 31 holds. I@16:54:22.895 State 1: state invariant 32 holds. I@16:54:23.015 State 1: state invariant 33 holds. I@16:54:23.019 State 1: state invariant 34 holds. I@16:54:23.025 State 1: state invariant 35 holds. I@16:54:23.041 State 1: Checking 14 state invariants I@16:54:23.273 State 1: state invariant 9 holds. I@16:54:23.277 State 1: state invariant 10 holds. I@16:54:23.279 State 1: state invariant 11 holds. I@16:54:23.280 State 1: state invariant 14 holds. I@16:54:23.288 State 1: state invariant 15 holds. I@16:54:23.290 State 1: state invariant 17 holds. I@16:54:23.291 State 1: state invariant 24 holds. I@16:54:23.293 State 1: state invariant 26 holds. I@16:54:23.295 State 1: state invariant 27 holds. I@16:54:23.301 State 1: state invariant 28 holds. I@16:54:23.315 State 1: state invariant 29 holds. I@16:54:23.322 State 1: state invariant 30 holds. I@16:54:23.378 State 1: state invariant 31 holds. I@16:54:23.452 State 1: state invariant 32 holds. I@16:54:23.515 State 1: Checking 26 state invariants I@16:54:23.640 State 1: state invariant 0 holds. I@16:54:23.641 State 1: state invariant 1 holds. I@16:54:23.665 State 1: state invariant 9 holds. I@16:54:23.672 State 1: state invariant 10 holds. I@16:54:23.674 State 1: state invariant 11 holds. I@16:54:23.675 State 1: state invariant 12 holds. I@16:54:23.682 State 1: state invariant 14 holds. I@16:54:23.693 State 1: state invariant 15 holds. I@16:54:23.697 State 1: state invariant 17 holds. I@16:54:23.699 State 1: state invariant 18 holds. I@16:54:23.708 State 1: state invariant 19 holds. I@16:54:23.719 State 1: state invariant 20 holds. I@16:54:23.727 State 1: state invariant 21 holds. I@16:54:23.741 State 1: state invariant 22 holds. I@16:54:23.749 State 1: state invariant 23 holds. I@16:54:23.758 State 1: state invariant 24 holds. I@16:54:23.760 State 1: state invariant 26 holds. I@16:54:23.764 State 1: state invariant 27 holds. I@16:54:23.784 State 1: state invariant 28 holds. I@16:54:23.820 State 1: state invariant 29 holds. I@16:54:23.829 State 1: state invariant 30 holds. I@16:54:24.005 State 1: state invariant 31 holds. I@16:54:24.160 State 1: state invariant 32 holds. I@16:54:24.345 State 1: state invariant 33 holds. I@16:54:24.349 State 1: state invariant 34 holds. I@16:54:24.359 State 1: state invariant 35 holds. I@16:54:24.371 State 1: Checking 22 state invariants I@16:54:24.503 State 1: state invariant 0 holds. I@16:54:24.504 State 1: state invariant 1 holds. I@16:54:24.528 State 1: state invariant 9 holds. I@16:54:24.536 State 1: state invariant 10 holds. I@16:54:24.538 State 1: state invariant 11 holds. I@16:54:24.540 State 1: state invariant 12 holds. I@16:54:24.546 State 1: state invariant 14 holds. I@16:54:24.558 State 1: state invariant 15 holds. I@16:54:24.564 State 1: state invariant 17 holds. I@16:54:24.567 State 1: state invariant 18 holds. I@16:54:24.574 State 1: state invariant 19 holds. I@16:54:24.592 State 1: state invariant 20 holds. I@16:54:24.603 State 1: state invariant 21 holds. I@16:54:24.614 State 1: state invariant 23 holds. I@16:54:24.623 State 1: state invariant 24 holds. I@16:54:24.625 State 1: state invariant 26 holds. I@16:54:24.633 State 1: state invariant 27 holds. I@16:54:24.659 State 1: state invariant 28 holds. I@16:54:24.706 State 1: state invariant 29 holds. I@16:54:24.715 State 1: state invariant 30 holds. I@16:54:24.928 State 1: state invariant 31 holds. I@16:54:25.087 State 1: state invariant 32 holds. I@16:54:25.237 Step 1: Transition #10 is disabled I@16:54:25.276 Step 1: Transition #11 is disabled I@16:54:25.316 State 1: Checking 27 state invariants I@16:54:25.455 State 1: state invariant 0 holds. I@16:54:25.457 State 1: state invariant 1 holds. I@16:54:25.480 State 1: state invariant 9 holds. I@16:54:25.488 State 1: state invariant 10 holds. I@16:54:25.490 State 1: state invariant 12 holds. I@16:54:25.496 State 1: state invariant 13 holds. I@16:54:25.497 State 1: state invariant 14 holds. I@16:54:25.505 State 1: state invariant 15 holds. I@16:54:25.519 State 1: state invariant 16 holds. I@16:54:25.520 State 1: state invariant 17 holds. I@16:54:25.522 State 1: state invariant 18 holds. I@16:54:25.528 State 1: state invariant 19 holds. I@16:54:25.539 State 1: state invariant 20 holds. I@16:54:25.550 State 1: state invariant 21 holds. I@16:54:25.561 State 1: state invariant 22 holds. I@16:54:25.572 State 1: state invariant 23 holds. I@16:54:25.581 State 1: state invariant 24 holds. I@16:54:25.583 State 1: state invariant 26 holds. I@16:54:25.586 State 1: state invariant 27 holds. I@16:54:25.607 State 1: state invariant 28 holds. I@16:54:25.633 State 1: state invariant 29 holds. I@16:54:25.641 State 1: state invariant 30 holds. I@16:54:25.765 State 1: state invariant 31 holds. I@16:54:25.907 State 1: state invariant 32 holds. I@16:54:26.026 State 1: state invariant 33 holds. I@16:54:26.031 State 1: state invariant 34 holds. I@16:54:26.038 State 1: state invariant 35 holds. I@16:54:26.048 State 1: Checking 23 state invariants I@16:54:26.314 State 1: state invariant 0 holds. I@16:54:26.316 State 1: state invariant 1 holds. I@16:54:26.341 State 1: state invariant 9 holds. I@16:54:26.351 State 1: state invariant 10 holds. I@16:54:26.353 State 1: state invariant 12 holds. I@16:54:26.360 State 1: state invariant 13 holds. I@16:54:26.361 State 1: state invariant 14 holds. I@16:54:26.369 State 1: state invariant 15 holds. I@16:54:26.374 State 1: state invariant 16 holds. I@16:54:26.375 State 1: state invariant 17 holds. I@16:54:26.376 State 1: state invariant 18 holds. I@16:54:26.382 State 1: state invariant 19 holds. I@16:54:26.400 State 1: state invariant 20 holds. I@16:54:26.407 State 1: state invariant 21 holds. I@16:54:26.420 State 1: state invariant 23 holds. I@16:54:26.429 State 1: state invariant 24 holds. I@16:54:26.431 State 1: state invariant 26 holds. I@16:54:26.437 State 1: state invariant 27 holds. I@16:54:26.446 State 1: state invariant 28 holds. I@16:54:26.468 State 1: state invariant 29 holds. I@16:54:26.476 State 1: state invariant 30 holds. I@16:54:26.647 State 1: state invariant 31 holds. I@16:54:26.809 State 1: state invariant 32 holds. I@16:54:26.922 State 1: Checking 26 state invariants I@16:54:27.164 State 1: state invariant 0 holds. I@16:54:27.167 State 1: state invariant 1 holds. I@16:54:27.193 State 1: state invariant 9 holds. I@16:54:27.208 State 1: state invariant 10 holds. I@16:54:27.210 State 1: state invariant 12 holds. I@16:54:27.219 State 1: state invariant 14 holds. I@16:54:27.227 State 1: state invariant 15 holds. I@16:54:27.229 State 1: state invariant 16 holds. I@16:54:27.230 State 1: state invariant 17 holds. I@16:54:27.232 State 1: state invariant 18 holds. I@16:54:27.241 State 1: state invariant 19 holds. I@16:54:27.256 State 1: state invariant 20 holds. I@16:54:27.266 State 1: state invariant 21 holds. I@16:54:27.291 State 1: state invariant 22 holds. I@16:54:27.306 State 1: state invariant 23 holds. I@16:54:27.315 State 1: state invariant 24 holds. I@16:54:27.317 State 1: state invariant 26 holds. I@16:54:27.322 State 1: state invariant 27 holds. I@16:54:27.338 State 1: state invariant 28 holds. I@16:54:27.368 State 1: state invariant 29 holds. I@16:54:27.376 State 1: state invariant 30 holds. I@16:54:27.507 State 1: state invariant 31 holds. I@16:54:27.641 State 1: state invariant 32 holds. I@16:54:27.824 State 1: state invariant 33 holds. I@16:54:27.834 State 1: state invariant 34 holds. I@16:54:27.845 State 1: state invariant 35 holds. I@16:54:27.867 State 1: Checking 22 state invariants I@16:54:28.127 State 1: state invariant 0 holds. I@16:54:28.128 State 1: state invariant 1 holds. I@16:54:28.157 State 1: state invariant 9 holds. I@16:54:28.164 State 1: state invariant 10 holds. I@16:54:28.165 State 1: state invariant 12 holds. I@16:54:28.172 State 1: state invariant 14 holds. I@16:54:28.180 State 1: state invariant 15 holds. I@16:54:28.189 State 1: state invariant 16 holds. I@16:54:28.190 State 1: state invariant 17 holds. I@16:54:28.192 State 1: state invariant 18 holds. I@16:54:28.198 State 1: state invariant 19 holds. I@16:54:28.207 State 1: state invariant 20 holds. I@16:54:28.213 State 1: state invariant 21 holds. I@16:54:28.226 State 1: state invariant 23 holds. I@16:54:28.234 State 1: state invariant 24 holds. I@16:54:28.236 State 1: state invariant 26 holds. I@16:54:28.243 State 1: state invariant 27 holds. I@16:54:28.259 State 1: state invariant 28 holds. I@16:54:28.281 State 1: state invariant 29 holds. I@16:54:28.289 State 1: state invariant 30 holds. I@16:54:28.407 State 1: state invariant 31 holds. I@16:54:28.510 State 1: state invariant 32 holds. I@16:54:28.614 Step 1: Transition #16 is disabled I@16:54:28.701 State 1: Checking 21 state invariants I@16:54:28.817 State 1: state invariant 0 holds. I@16:54:28.819 State 1: state invariant 1 holds. I@16:54:28.851 State 1: state invariant 9 holds. I@16:54:28.863 State 1: state invariant 10 holds. I@16:54:28.866 State 1: state invariant 12 holds. I@16:54:28.873 State 1: state invariant 14 holds. I@16:54:28.882 State 1: state invariant 15 holds. I@16:54:28.892 State 1: state invariant 17 holds. I@16:54:28.894 State 1: state invariant 18 holds. I@16:54:28.911 State 1: state invariant 19 holds. I@16:54:28.926 State 1: state invariant 20 holds. I@16:54:28.939 State 1: state invariant 21 holds. I@16:54:28.958 State 1: state invariant 23 holds. I@16:54:28.968 State 1: state invariant 24 holds. I@16:54:28.971 State 1: state invariant 26 holds. I@16:54:28.974 State 1: state invariant 27 holds. I@16:54:28.989 State 1: state invariant 28 holds. I@16:54:29.040 State 1: state invariant 29 holds. I@16:54:29.050 State 1: state invariant 30 holds. I@16:54:29.221 State 1: state invariant 31 holds. I@16:54:29.385 State 1: state invariant 32 holds. I@16:54:29.535 Step 1: Transition #18 is disabled I@16:54:29.577 State 1: Checking 21 state invariants I@16:54:29.644 State 1: state invariant 0 holds. I@16:54:29.646 State 1: state invariant 1 holds. I@16:54:29.671 State 1: state invariant 9 holds. I@16:54:29.679 State 1: state invariant 10 holds. I@16:54:29.682 State 1: state invariant 12 holds. I@16:54:29.689 State 1: state invariant 14 holds. I@16:54:29.698 State 1: state invariant 15 holds. I@16:54:29.706 State 1: state invariant 17 holds. I@16:54:29.708 State 1: state invariant 18 holds. I@16:54:29.718 State 1: state invariant 19 holds. I@16:54:29.734 State 1: state invariant 20 holds. I@16:54:29.764 State 1: state invariant 21 holds. I@16:54:29.791 State 1: state invariant 23 holds. I@16:54:29.801 State 1: state invariant 24 holds. I@16:54:29.804 State 1: state invariant 26 holds. I@16:54:29.807 State 1: state invariant 27 holds. I@16:54:29.832 State 1: state invariant 28 holds. I@16:54:29.879 State 1: state invariant 29 holds. I@16:54:29.889 State 1: state invariant 30 holds. I@16:54:30.157 State 1: state invariant 31 holds. I@16:54:30.347 State 1: state invariant 32 holds. I@16:54:30.501 Step 1: Transition #20 is disabled I@16:54:30.540 Step 1: Transition #21 is disabled I@16:54:30.602 State 1: Checking 14 state invariants I@16:54:30.686 State 1: state invariant 6 holds. I@16:54:30.687 State 1: state invariant 7 holds. I@16:54:30.690 State 1: state invariant 22 holds. I@16:54:30.702 State 1: state invariant 25 holds. I@16:54:30.706 State 1: state invariant 27 holds. I@16:54:30.730 State 1: state invariant 28 holds. I@16:54:30.761 State 1: state invariant 29 holds. I@16:54:30.769 State 1: state invariant 30 holds. I@16:54:30.884 State 1: state invariant 31 holds. I@16:54:30.965 State 1: state invariant 32 holds. I@16:54:31.065 State 1: state invariant 33 holds. I@16:54:31.071 State 1: state invariant 34 holds. I@16:54:31.077 State 1: state invariant 35 holds. I@16:54:31.082 State 1: state invariant 38 holds. I@16:54:31.084 State 1: Checking 17 state invariants I@16:54:31.167 State 1: state invariant 3 holds. I@16:54:31.172 State 1: state invariant 4 holds. I@16:54:31.213 State 1: state invariant 5 holds. I@16:54:31.241 State 1: state invariant 6 holds. I@16:54:31.244 State 1: state invariant 7 holds. I@16:54:31.246 State 1: state invariant 22 holds. I@16:54:31.261 State 1: state invariant 25 holds. I@16:54:31.263 State 1: state invariant 27 holds. I@16:54:31.269 State 1: state invariant 28 holds. I@16:54:31.315 State 1: state invariant 29 holds. I@16:54:31.323 State 1: state invariant 30 holds. I@16:54:31.612 State 1: state invariant 31 holds. I@16:54:31.818 State 1: state invariant 32 holds. I@16:54:32.240 State 1: state invariant 33 holds. I@16:54:32.256 State 1: state invariant 34 holds. I@16:54:32.262 State 1: state invariant 35 holds. I@16:54:32.267 State 1: state invariant 38 holds. I@16:54:32.269 Step 1: picking a transition out of 17 transition(s) I@16:54:32.270 The outcome is: NoError I@16:54:32.416 > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... PASS #0: SanyParser I@16:54:32.626 PASS #1: TypeCheckerSnowcat I@16:54:32.705 > Running Snowcat .::. I@16:54:32.705 > Your types are purrfect! I@16:54:34.848 > All expressions are typed I@16:54:34.849 PASS #2: ConfigurationPass I@16:54:34.849 > Set the initialization predicate to q::inductiveInv I@16:54:34.850 > Set the transition predicate to q::step I@16:54:34.850 > Set an invariant to q::inv I@16:54:34.850 PASS #3: DesugarerPass I@16:54:34.852 > Desugaring... I@16:54:34.852 PASS #4: InlinePass I@16:54:34.853 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:54:34.853 PASS #5: TemporalPass I@16:54:34.880 > Rewriting temporal operators... I@16:54:34.880 > No temporal property specified, nothing to encode I@16:54:34.880 PASS #6: InlinePass I@16:54:34.880 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:54:34.880 PASS #7: PrimingPass I@16:54:34.891 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:34.891 PASS #8: VCGen I@16:54:34.892 > Producing verification conditions from the invariant q::inv I@16:54:34.892 > VCGen produced 5 verification condition(s) I@16:54:34.893 PASS #9: PreprocessingPass I@16:54:34.893 > Before preprocessing: unique renaming I@16:54:34.893 > Applying standard transformations: I@16:54:34.893 > PrimePropagation I@16:54:34.894 > Desugarer I@16:54:34.897 > UniqueRenamer I@16:54:34.904 > Normalizer I@16:54:34.914 > SetMembershipSimplifier I@16:54:34.919 > Keramelizer I@16:54:34.922 > After preprocessing: UniqueRenamer I@16:54:34.929 PASS #10: TransitionFinderPass I@16:54:34.942 > Found 1 initializing transitions I@16:54:34.943 > Found 24 transitions I@16:54:34.952 > No constant initializer I@16:54:34.952 > Applying unique renaming I@16:54:34.952 PASS #11: OptimizationPass I@16:54:34.968 > Applying optimizations: I@16:54:34.969 > ConstSimplifier I@16:54:34.969 > ExprOptimizer I@16:54:35.030 > SetMembershipSimplifier I@16:54:35.036 > ConstSimplifier I@16:54:35.039 PASS #12: AnalysisPass I@16:54:35.096 > Marking skolemizable existentials and sets to be expanded... I@16:54:35.096 > Skolemization I@16:54:35.096 > Expansion I@16:54:35.099 > Remove unused let-in defs I@16:54:35.108 > Running analyzers... I@16:54:35.111 > Introduced expression grades I@16:54:35.112 PASS #13: BoundedChecker I@16:54:35.112 State 0: Checking 5 state invariants I@16:54:35.657 State 0: state invariant 0 holds. I@16:54:35.658 State 0: state invariant 1 holds. I@16:54:35.659 State 0: state invariant 2 holds. I@16:54:35.660 State 0: state invariant 3 holds. I@16:54:35.665 State 0: state invariant 4 holds. I@16:54:35.697 Step 0: picking a transition out of 1 transition(s) I@16:54:35.698 The outcome is: NoError I@16:54:35.708 [ok] No violation found (29526ms). You may increase --max-steps. Use --verbosity to produce more (or less) output.