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-08-25T09-12-55_4033946123800500636 # APALACHE version: 0.56.1 | build: 70cdaf4 I@09:12:55.604 Starting checker server on port 8822... I@09:12:55.613 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: 23:92:16:4e:ef:62:66:8b W@09:12:56.288 Aug 25, 2026 9:12:59 AM 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@09:12:59.515 PASS #1: TypeCheckerSnowcat I@09:13:00.137 > Running Snowcat .::. I@09:13:00.137 > Your types are purrfect! I@09:13:02.041 > All expressions are typed I@09:13:02.042 PASS #2: ConfigurationPass I@09:13:02.043 > Set the initialization predicate to q::init I@09:13:02.048 > Set the transition predicate to q::step I@09:13:02.049 > Set an invariant to q::inductiveInv I@09:13:02.049 PASS #3: DesugarerPass I@09:13:02.056 > Desugaring... I@09:13:02.056 PASS #4: InlinePass I@09:13:02.071 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@09:13:02.072 PASS #5: TemporalPass I@09:13:02.175 > Rewriting temporal operators... I@09:13:02.175 > No temporal property specified, nothing to encode I@09:13:02.175 PASS #6: InlinePass I@09:13:02.175 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@09:13:02.175 PASS #7: PrimingPass I@09:13:02.204 > Introducing q::initPrimed for q::init' I@09:13:02.207 PASS #8: VCGen I@09:13:02.209 > Producing verification conditions from the invariant q::inductiveInv I@09:13:02.209 > VCGen produced 35 verification condition(s) I@09:13:02.218 PASS #9: PreprocessingPass I@09:13:02.221 > Before preprocessing: unique renaming I@09:13:02.221 > Applying standard transformations: I@09:13:02.229 > PrimePropagation I@09:13:02.229 > Desugarer I@09:13:02.235 > UniqueRenamer I@09:13:02.245 > Normalizer I@09:13:02.265 > Keramelizer I@09:13:02.283 > After preprocessing: UniqueRenamer I@09:13:02.307 PASS #10: TransitionFinderPass I@09:13:02.345 > Found 1 initializing transitions I@09:13:02.358 > Found 18 transitions I@09:13:02.386 > No constant initializer I@09:13:02.386 > Applying unique renaming I@09:13:02.387 PASS #11: OptimizationPass I@09:13:02.415 > Applying optimizations: I@09:13:02.423 > ConstSimplifier I@09:13:02.424 > ExprOptimizer I@09:13:02.477 > SetMembershipSimplifier I@09:13:02.501 > ConstSimplifier I@09:13:02.509 PASS #12: AnalysisPass I@09:13:02.555 > Marking skolemizable existentials and sets to be expanded... I@09:13:02.558 > Skolemization I@09:13:02.558 > Expansion I@09:13:02.564 > Remove unused let-in defs I@09:13:02.580 > Running analyzers... I@09:13:02.591 > Introduced expression grades I@09:13:02.602 PASS #13: BoundedChecker I@09:13:02.602 State 0: Checking 35 state invariants I@09:13:03.106 State 0: state invariant 0 holds. I@09:13:03.109 State 0: state invariant 1 holds. I@09:13:03.150 State 0: state invariant 2 holds. I@09:13:03.151 State 0: state invariant 3 holds. I@09:13:03.152 State 0: state invariant 4 holds. I@09:13:03.154 State 0: state invariant 5 holds. I@09:13:03.161 State 0: state invariant 6 holds. I@09:13:03.162 State 0: state invariant 7 holds. I@09:13:03.162 State 0: state invariant 8 holds. I@09:13:03.163 State 0: state invariant 9 holds. I@09:13:03.172 State 0: state invariant 10 holds. I@09:13:03.173 State 0: state invariant 11 holds. I@09:13:03.174 State 0: state invariant 12 holds. I@09:13:03.182 State 0: state invariant 13 holds. I@09:13:03.183 State 0: state invariant 14 holds. I@09:13:03.186 State 0: state invariant 15 holds. I@09:13:03.192 State 0: state invariant 16 holds. I@09:13:03.199 State 0: state invariant 17 holds. I@09:13:03.204 State 0: state invariant 18 holds. I@09:13:03.209 State 0: state invariant 19 holds. I@09:13:03.211 State 0: state invariant 20 holds. I@09:13:03.211 State 0: state invariant 21 holds. I@09:13:03.218 State 0: state invariant 22 holds. I@09:13:03.228 State 0: state invariant 23 holds. I@09:13:03.236 State 0: state invariant 24 holds. I@09:13:03.258 State 0: state invariant 25 holds. I@09:13:03.264 State 0: state invariant 26 holds. I@09:13:03.283 State 0: state invariant 27 holds. I@09:13:03.307 State 0: state invariant 28 holds. I@09:13:03.333 State 0: state invariant 29 holds. I@09:13:03.334 State 0: state invariant 30 holds. I@09:13:03.344 State 0: state invariant 31 holds. I@09:13:03.354 State 0: state invariant 32 holds. I@09:13:03.355 State 0: state invariant 33 holds. I@09:13:03.355 State 0: state invariant 34 holds. I@09:13:03.356 Step 0: picking a transition out of 1 transition(s) I@09:13:03.356 The outcome is: NoError I@09:13:03.365 > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... PASS #0: SanyParser I@09:13:03.686 PASS #1: TypeCheckerSnowcat I@09:13:03.789 > Running Snowcat .::. I@09:13:03.789 > Your types are purrfect! I@09:13:05.561 > All expressions are typed I@09:13:05.562 PASS #2: ConfigurationPass I@09:13:05.562 > Set the initialization predicate to q::inductiveInv I@09:13:05.563 > Set the transition predicate to q::step I@09:13:05.563 > Set an invariant to q::inductiveInv I@09:13:05.563 PASS #3: DesugarerPass I@09:13:05.565 > Desugaring... I@09:13:05.565 PASS #4: InlinePass I@09:13:05.567 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@09:13:05.567 PASS #5: TemporalPass I@09:13:05.594 > Rewriting temporal operators... I@09:13:05.594 > No temporal property specified, nothing to encode I@09:13:05.594 PASS #6: InlinePass I@09:13:05.594 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@09:13:05.594 PASS #7: PrimingPass I@09:13:05.602 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@09:13:05.603 PASS #8: VCGen I@09:13:05.604 > Producing verification conditions from the invariant q::inductiveInv I@09:13:05.604 > VCGen produced 35 verification condition(s) I@09:13:05.605 PASS #9: PreprocessingPass I@09:13:05.606 > Before preprocessing: unique renaming I@09:13:05.606 > Applying standard transformations: I@09:13:05.606 > PrimePropagation I@09:13:05.606 > Desugarer I@09:13:05.608 > UniqueRenamer I@09:13:05.614 > Normalizer I@09:13:05.623 > Keramelizer I@09:13:05.637 > After preprocessing: UniqueRenamer I@09:13:05.646 PASS #10: TransitionFinderPass I@09:13:05.658 > Found 1 initializing transitions I@09:13:05.661 > Found 18 transitions I@09:13:05.670 > No constant initializer I@09:13:05.670 > Applying unique renaming I@09:13:05.670 PASS #11: OptimizationPass I@09:13:05.688 > Applying optimizations: I@09:13:05.688 > ConstSimplifier I@09:13:05.688 > ExprOptimizer I@09:13:05.746 > SetMembershipSimplifier I@09:13:05.758 > ConstSimplifier I@09:13:05.762 PASS #12: AnalysisPass I@09:13:05.813 > Marking skolemizable existentials and sets to be expanded... I@09:13:05.814 > Skolemization I@09:13:05.814 > Expansion I@09:13:05.817 > Remove unused let-in defs I@09:13:05.828 > Running analyzers... I@09:13:05.831 > Introduced expression grades I@09:13:05.833 PASS #13: BoundedChecker I@09:13:05.833 State 0: Checking 35 state invariants I@09:13:06.335 State 0: state invariant 0 holds. I@09:13:06.336 State 0: state invariant 1 holds. I@09:13:06.355 State 0: state invariant 2 holds. I@09:13:06.357 State 0: state invariant 3 holds. I@09:13:06.358 State 0: state invariant 4 holds. I@09:13:06.359 State 0: state invariant 5 holds. I@09:13:06.362 State 0: state invariant 6 holds. I@09:13:06.364 State 0: state invariant 7 holds. I@09:13:06.365 State 0: state invariant 8 holds. I@09:13:06.367 State 0: state invariant 9 holds. I@09:13:06.374 State 0: state invariant 10 holds. I@09:13:06.375 State 0: state invariant 11 holds. I@09:13:06.376 State 0: state invariant 12 holds. I@09:13:06.382 State 0: state invariant 13 holds. I@09:13:06.383 State 0: state invariant 14 holds. I@09:13:06.388 State 0: state invariant 15 holds. I@09:13:06.394 State 0: state invariant 16 holds. I@09:13:06.406 State 0: state invariant 17 holds. I@09:13:06.416 State 0: state invariant 18 holds. I@09:13:06.425 State 0: state invariant 19 holds. I@09:13:06.426 State 0: state invariant 20 holds. I@09:13:06.426 State 0: state invariant 21 holds. I@09:13:06.428 State 0: state invariant 22 holds. I@09:13:06.432 State 0: state invariant 23 holds. I@09:13:06.440 State 0: state invariant 24 holds. I@09:13:06.494 State 0: state invariant 25 holds. I@09:13:06.501 State 0: state invariant 26 holds. I@09:13:06.600 State 0: state invariant 27 holds. I@09:13:06.666 State 0: state invariant 28 holds. I@09:13:06.787 State 0: state invariant 29 holds. I@09:13:06.790 State 0: state invariant 30 holds. I@09:13:06.803 State 0: state invariant 31 holds. I@09:13:06.818 State 0: state invariant 32 holds. I@09:13:06.819 State 0: state invariant 33 holds. I@09:13:06.820 State 0: state invariant 34 holds. I@09:13:06.821 Step 0: picking a transition out of 1 transition(s) I@09:13:06.822 State 1: Checking 4 state invariants I@09:13:06.834 State 1: state invariant 8 holds. I@09:13:06.835 State 1: state invariant 25 holds. I@09:13:06.840 State 1: state invariant 26 holds. I@09:13:06.949 State 1: state invariant 27 holds. I@09:13:07.018 State 1: Checking 15 state invariants I@09:13:07.034 State 1: state invariant 0 holds. I@09:13:07.035 State 1: state invariant 1 holds. I@09:13:07.052 State 1: state invariant 12 holds. I@09:13:07.060 State 1: state invariant 14 holds. I@09:13:07.068 State 1: state invariant 15 holds. I@09:13:07.073 State 1: state invariant 16 holds. I@09:13:07.080 State 1: state invariant 17 holds. I@09:13:07.091 State 1: state invariant 22 holds. I@09:13:07.099 State 1: state invariant 24 holds. I@09:13:07.148 State 1: state invariant 25 holds. I@09:13:07.155 State 1: state invariant 26 holds. I@09:13:07.239 State 1: state invariant 27 holds. I@09:13:07.309 State 1: state invariant 28 holds. I@09:13:07.389 State 1: state invariant 33 holds. I@09:13:07.392 State 1: state invariant 34 holds. I@09:13:07.393 State 1: Checking 18 state invariants I@09:13:07.532 State 1: state invariant 5 holds. I@09:13:07.536 State 1: state invariant 6 holds. I@09:13:07.538 State 1: state invariant 7 holds. I@09:13:07.539 State 1: state invariant 9 holds. I@09:13:07.545 State 1: state invariant 10 holds. I@09:13:07.546 State 1: state invariant 13 holds. I@09:13:07.547 State 1: state invariant 18 holds. I@09:13:07.557 State 1: state invariant 19 holds. I@09:13:07.558 State 1: state invariant 21 holds. I@09:13:07.560 State 1: state invariant 22 holds. I@09:13:07.569 State 1: state invariant 24 holds. I@09:13:07.606 State 1: state invariant 25 holds. I@09:13:07.612 State 1: state invariant 26 holds. I@09:13:07.659 State 1: state invariant 27 holds. I@09:13:07.693 State 1: state invariant 28 holds. I@09:13:07.756 State 1: state invariant 29 holds. I@09:13:07.759 State 1: state invariant 30 holds. I@09:13:07.776 State 1: state invariant 31 holds. I@09:13:07.816 State 1: Checking 14 state invariants I@09:13:07.928 State 1: state invariant 5 holds. I@09:13:07.932 State 1: state invariant 6 holds. I@09:13:07.934 State 1: state invariant 7 holds. I@09:13:07.936 State 1: state invariant 9 holds. I@09:13:07.942 State 1: state invariant 10 holds. I@09:13:07.944 State 1: state invariant 13 holds. I@09:13:07.945 State 1: state invariant 19 holds. I@09:13:07.947 State 1: state invariant 21 holds. I@09:13:07.949 State 1: state invariant 22 holds. I@09:13:07.954 State 1: state invariant 24 holds. I@09:13:07.974 State 1: state invariant 25 holds. I@09:13:07.980 State 1: state invariant 26 holds. I@09:13:08.114 State 1: state invariant 27 holds. I@09:13:08.146 State 1: state invariant 28 holds. I@09:13:08.188 State 1: Checking 26 state invariants I@09:13:08.285 State 1: state invariant 0 holds. I@09:13:08.286 State 1: state invariant 1 holds. I@09:13:08.304 State 1: state invariant 5 holds. I@09:13:08.309 State 1: state invariant 6 holds. I@09:13:08.310 State 1: state invariant 7 holds. I@09:13:08.311 State 1: state invariant 9 holds. I@09:13:08.318 State 1: state invariant 10 holds. I@09:13:08.333 State 1: state invariant 12 holds. I@09:13:08.339 State 1: state invariant 13 holds. I@09:13:08.340 State 1: state invariant 14 holds. I@09:13:08.346 State 1: state invariant 15 holds. I@09:13:08.361 State 1: state invariant 16 holds. I@09:13:08.367 State 1: state invariant 17 holds. I@09:13:08.381 State 1: state invariant 18 holds. I@09:13:08.396 State 1: state invariant 19 holds. I@09:13:08.398 State 1: state invariant 21 holds. I@09:13:08.400 State 1: state invariant 22 holds. I@09:13:08.417 State 1: state invariant 23 holds. I@09:13:08.424 State 1: state invariant 24 holds. I@09:13:08.484 State 1: state invariant 25 holds. I@09:13:08.491 State 1: state invariant 26 holds. I@09:13:08.590 State 1: state invariant 27 holds. I@09:13:08.664 State 1: state invariant 28 holds. I@09:13:08.773 State 1: state invariant 29 holds. I@09:13:08.776 State 1: state invariant 30 holds. I@09:13:08.792 State 1: state invariant 31 holds. I@09:13:08.844 State 1: Checking 22 state invariants I@09:13:08.937 State 1: state invariant 0 holds. I@09:13:08.939 State 1: state invariant 1 holds. I@09:13:08.958 State 1: state invariant 5 holds. I@09:13:08.963 State 1: state invariant 6 holds. I@09:13:08.965 State 1: state invariant 7 holds. I@09:13:08.966 State 1: state invariant 9 holds. I@09:13:08.974 State 1: state invariant 10 holds. I@09:13:08.978 State 1: state invariant 12 holds. I@09:13:08.983 State 1: state invariant 13 holds. I@09:13:08.985 State 1: state invariant 14 holds. I@09:13:08.991 State 1: state invariant 15 holds. I@09:13:08.997 State 1: state invariant 16 holds. I@09:13:09.003 State 1: state invariant 17 holds. I@09:13:09.012 State 1: state invariant 19 holds. I@09:13:09.014 State 1: state invariant 21 holds. I@09:13:09.017 State 1: state invariant 22 holds. I@09:13:09.029 State 1: state invariant 23 holds. I@09:13:09.036 State 1: state invariant 24 holds. I@09:13:09.092 State 1: state invariant 25 holds. I@09:13:09.099 State 1: state invariant 26 holds. I@09:13:09.214 State 1: state invariant 27 holds. I@09:13:09.282 State 1: state invariant 28 holds. I@09:13:09.369 Step 1: Transition #6 is disabled I@09:13:09.404 Step 1: Transition #7 is disabled I@09:13:09.431 State 1: Checking 27 state invariants I@09:13:09.538 State 1: state invariant 0 holds. I@09:13:09.539 State 1: state invariant 1 holds. I@09:13:09.552 State 1: state invariant 5 holds. I@09:13:09.559 State 1: state invariant 6 holds. I@09:13:09.560 State 1: state invariant 8 holds. I@09:13:09.561 State 1: state invariant 9 holds. I@09:13:09.566 State 1: state invariant 10 holds. I@09:13:09.574 State 1: state invariant 11 holds. I@09:13:09.575 State 1: state invariant 12 holds. I@09:13:09.580 State 1: state invariant 13 holds. I@09:13:09.581 State 1: state invariant 14 holds. I@09:13:09.586 State 1: state invariant 15 holds. I@09:13:09.594 State 1: state invariant 16 holds. I@09:13:09.601 State 1: state invariant 17 holds. I@09:13:09.608 State 1: state invariant 18 holds. I@09:13:09.624 State 1: state invariant 19 holds. I@09:13:09.626 State 1: state invariant 21 holds. I@09:13:09.629 State 1: state invariant 22 holds. I@09:13:09.641 State 1: state invariant 23 holds. I@09:13:09.648 State 1: state invariant 24 holds. I@09:13:09.710 State 1: state invariant 25 holds. I@09:13:09.716 State 1: state invariant 26 holds. I@09:13:09.805 State 1: state invariant 27 holds. I@09:13:09.863 State 1: state invariant 28 holds. I@09:13:09.959 State 1: state invariant 29 holds. I@09:13:09.962 State 1: state invariant 30 holds. I@09:13:09.976 State 1: state invariant 31 holds. I@09:13:10.022 State 1: Checking 23 state invariants I@09:13:10.103 State 1: state invariant 0 holds. I@09:13:10.104 State 1: state invariant 1 holds. I@09:13:10.118 State 1: state invariant 5 holds. I@09:13:10.125 State 1: state invariant 6 holds. I@09:13:10.126 State 1: state invariant 8 holds. I@09:13:10.127 State 1: state invariant 9 holds. I@09:13:10.133 State 1: state invariant 10 holds. I@09:13:10.140 State 1: state invariant 11 holds. I@09:13:10.142 State 1: state invariant 12 holds. I@09:13:10.146 State 1: state invariant 13 holds. I@09:13:10.147 State 1: state invariant 14 holds. I@09:13:10.154 State 1: state invariant 15 holds. I@09:13:10.162 State 1: state invariant 16 holds. I@09:13:10.169 State 1: state invariant 17 holds. I@09:13:10.177 State 1: state invariant 19 holds. I@09:13:10.179 State 1: state invariant 21 holds. I@09:13:10.181 State 1: state invariant 22 holds. I@09:13:10.187 State 1: state invariant 23 holds. I@09:13:10.194 State 1: state invariant 24 holds. I@09:13:10.223 State 1: state invariant 25 holds. I@09:13:10.228 State 1: state invariant 26 holds. I@09:13:10.325 State 1: state invariant 27 holds. I@09:13:10.394 State 1: state invariant 28 holds. I@09:13:10.474 State 1: Checking 26 state invariants I@09:13:10.638 State 1: state invariant 0 holds. I@09:13:10.639 State 1: state invariant 1 holds. I@09:13:10.652 State 1: state invariant 5 holds. I@09:13:10.659 State 1: state invariant 6 holds. I@09:13:10.660 State 1: state invariant 9 holds. I@09:13:10.666 State 1: state invariant 10 holds. I@09:13:10.669 State 1: state invariant 11 holds. I@09:13:10.670 State 1: state invariant 12 holds. I@09:13:10.675 State 1: state invariant 13 holds. I@09:13:10.676 State 1: state invariant 14 holds. I@09:13:10.682 State 1: state invariant 15 holds. I@09:13:10.685 State 1: state invariant 16 holds. I@09:13:10.690 State 1: state invariant 17 holds. I@09:13:10.698 State 1: state invariant 18 holds. I@09:13:10.710 State 1: state invariant 19 holds. I@09:13:10.712 State 1: state invariant 21 holds. I@09:13:10.714 State 1: state invariant 22 holds. I@09:13:10.724 State 1: state invariant 23 holds. I@09:13:10.731 State 1: state invariant 24 holds. I@09:13:10.769 State 1: state invariant 25 holds. I@09:13:10.775 State 1: state invariant 26 holds. I@09:13:10.842 State 1: state invariant 27 holds. I@09:13:10.886 State 1: state invariant 28 holds. I@09:13:10.957 State 1: state invariant 29 holds. I@09:13:10.969 State 1: state invariant 30 holds. I@09:13:10.981 State 1: state invariant 31 holds. I@09:13:11.024 State 1: Checking 22 state invariants I@09:13:11.170 State 1: state invariant 0 holds. I@09:13:11.172 State 1: state invariant 1 holds. I@09:13:11.188 State 1: state invariant 5 holds. I@09:13:11.197 State 1: state invariant 6 holds. I@09:13:11.198 State 1: state invariant 9 holds. I@09:13:11.204 State 1: state invariant 10 holds. I@09:13:11.206 State 1: state invariant 11 holds. I@09:13:11.207 State 1: state invariant 12 holds. I@09:13:11.213 State 1: state invariant 13 holds. I@09:13:11.214 State 1: state invariant 14 holds. I@09:13:11.223 State 1: state invariant 15 holds. I@09:13:11.230 State 1: state invariant 16 holds. I@09:13:11.242 State 1: state invariant 17 holds. I@09:13:11.255 State 1: state invariant 19 holds. I@09:13:11.257 State 1: state invariant 21 holds. I@09:13:11.261 State 1: state invariant 22 holds. I@09:13:11.274 State 1: state invariant 23 holds. I@09:13:11.281 State 1: state invariant 24 holds. I@09:13:11.310 State 1: state invariant 25 holds. I@09:13:11.316 State 1: state invariant 26 holds. I@09:13:11.420 State 1: state invariant 27 holds. I@09:13:11.479 State 1: state invariant 28 holds. I@09:13:11.547 Step 1: Transition #12 is disabled I@09:13:11.581 State 1: Checking 21 state invariants I@09:13:11.671 State 1: state invariant 0 holds. I@09:13:11.672 State 1: state invariant 1 holds. I@09:13:11.689 State 1: state invariant 5 holds. I@09:13:11.697 State 1: state invariant 6 holds. I@09:13:11.698 State 1: state invariant 9 holds. I@09:13:11.704 State 1: state invariant 10 holds. I@09:13:11.710 State 1: state invariant 12 holds. I@09:13:11.717 State 1: state invariant 13 holds. I@09:13:11.719 State 1: state invariant 14 holds. I@09:13:11.725 State 1: state invariant 15 holds. I@09:13:11.736 State 1: state invariant 16 holds. I@09:13:11.753 State 1: state invariant 17 holds. I@09:13:11.769 State 1: state invariant 19 holds. I@09:13:11.771 State 1: state invariant 21 holds. I@09:13:11.773 State 1: state invariant 22 holds. I@09:13:11.782 State 1: state invariant 23 holds. I@09:13:11.789 State 1: state invariant 24 holds. I@09:13:11.830 State 1: state invariant 25 holds. I@09:13:11.837 State 1: state invariant 26 holds. I@09:13:11.960 State 1: state invariant 27 holds. I@09:13:12.049 State 1: state invariant 28 holds. I@09:13:12.162 Step 1: Transition #14 is disabled I@09:13:12.196 Step 1: Transition #15 is disabled I@09:13:12.245 State 1: Checking 14 state invariants I@09:13:12.301 State 1: state invariant 2 holds. I@09:13:12.302 State 1: state invariant 3 holds. I@09:13:12.304 State 1: state invariant 18 holds. I@09:13:12.311 State 1: state invariant 20 holds. I@09:13:12.312 State 1: state invariant 22 holds. I@09:13:12.317 State 1: state invariant 24 holds. I@09:13:12.337 State 1: state invariant 25 holds. I@09:13:12.343 State 1: state invariant 26 holds. I@09:13:12.393 State 1: state invariant 27 holds. I@09:13:12.422 State 1: state invariant 28 holds. I@09:13:12.462 State 1: state invariant 29 holds. I@09:13:12.467 State 1: state invariant 30 holds. I@09:13:12.479 State 1: state invariant 31 holds. I@09:13:12.492 State 1: state invariant 34 holds. I@09:13:12.494 State 1: Checking 21 state invariants I@09:13:12.550 State 1: state invariant 0 holds. I@09:13:12.551 State 1: state invariant 1 holds. I@09:13:12.572 State 1: state invariant 2 holds. I@09:13:12.574 State 1: state invariant 3 holds. I@09:13:12.575 State 1: state invariant 14 holds. I@09:13:12.582 State 1: state invariant 15 holds. I@09:13:12.588 State 1: state invariant 16 holds. I@09:13:12.597 State 1: state invariant 17 holds. I@09:13:12.609 State 1: state invariant 18 holds. I@09:13:12.623 State 1: state invariant 20 holds. I@09:13:12.624 State 1: state invariant 22 holds. I@09:13:12.628 State 1: state invariant 23 holds. I@09:13:12.637 State 1: state invariant 24 holds. I@09:13:12.699 State 1: state invariant 25 holds. I@09:13:12.707 State 1: state invariant 26 holds. I@09:13:12.882 State 1: state invariant 27 holds. I@09:13:12.945 State 1: state invariant 28 holds. I@09:13:13.039 State 1: state invariant 29 holds. I@09:13:13.043 State 1: state invariant 30 holds. I@09:13:13.055 State 1: state invariant 31 holds. I@09:13:13.069 State 1: state invariant 34 holds. I@09:13:13.071 Step 1: picking a transition out of 13 transition(s) I@09:13:13.073 The outcome is: NoError I@09:13:13.235 > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... PASS #0: SanyParser I@09:13:13.404 PASS #1: TypeCheckerSnowcat I@09:13:13.477 > Running Snowcat .::. I@09:13:13.477 > Your types are purrfect! I@09:13:14.875 > All expressions are typed I@09:13:14.876 PASS #2: ConfigurationPass I@09:13:14.876 > Set the initialization predicate to q::inductiveInv I@09:13:14.877 > Set the transition predicate to q::step I@09:13:14.877 > Set an invariant to q::inv I@09:13:14.877 PASS #3: DesugarerPass I@09:13:14.878 > Desugaring... I@09:13:14.878 PASS #4: InlinePass I@09:13:14.879 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@09:13:14.880 PASS #5: TemporalPass I@09:13:14.901 > Rewriting temporal operators... I@09:13:14.902 > No temporal property specified, nothing to encode I@09:13:14.902 PASS #6: InlinePass I@09:13:14.902 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@09:13:14.902 PASS #7: PrimingPass I@09:13:14.910 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@09:13:14.910 PASS #8: VCGen I@09:13:14.911 > Producing verification conditions from the invariant q::inv I@09:13:14.911 > VCGen produced 5 verification condition(s) I@09:13:14.912 PASS #9: PreprocessingPass I@09:13:14.912 > Before preprocessing: unique renaming I@09:13:14.912 > Applying standard transformations: I@09:13:14.912 > PrimePropagation I@09:13:14.912 > Desugarer I@09:13:14.914 > UniqueRenamer I@09:13:14.917 > Normalizer I@09:13:14.925 > Keramelizer I@09:13:14.929 > After preprocessing: UniqueRenamer I@09:13:14.936 PASS #10: TransitionFinderPass I@09:13:14.945 > Found 1 initializing transitions I@09:13:14.946 > Found 18 transitions I@09:13:14.952 > No constant initializer I@09:13:14.952 > Applying unique renaming I@09:13:14.953 PASS #11: OptimizationPass I@09:13:14.964 > Applying optimizations: I@09:13:14.964 > ConstSimplifier I@09:13:14.964 > ExprOptimizer I@09:13:15.006 > SetMembershipSimplifier I@09:13:15.012 > ConstSimplifier I@09:13:15.014 PASS #12: AnalysisPass I@09:13:15.055 > Marking skolemizable existentials and sets to be expanded... I@09:13:15.055 > Skolemization I@09:13:15.055 > Expansion I@09:13:15.057 > Remove unused let-in defs I@09:13:15.062 > Running analyzers... I@09:13:15.064 > Introduced expression grades I@09:13:15.065 PASS #13: BoundedChecker I@09:13:15.065 State 0: Checking 5 state invariants I@09:13:15.408 State 0: state invariant 0 holds. I@09:13:15.409 State 0: state invariant 1 holds. I@09:13:15.410 State 0: state invariant 2 holds. I@09:13:15.411 State 0: state invariant 3 holds. I@09:13:15.415 State 0: state invariant 4 holds. I@09:13:15.469 Step 0: picking a transition out of 1 transition(s) I@09:13:15.471 The outcome is: NoError I@09:13:15.482 [ok] No violation found (20546ms). You may increase --max-steps. Use --verbosity to produce more (or less) output.