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