this derivation will be built: /nix/store/xpgf0llrlacw7xpds5pgas2ldzkp5swv-spec-protocol.drv building '/nix/store/xpgf0llrlacw7xpds5pgas2ldzkp5swv-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-25T08-54-50_4577010489392133844 spec-protocol> # APALACHE version: 0.56.1 | build: 70cdaf4 I@08:54:50.762 spec-protocol> Starting checker server on port 8822... I@08:54:50.772 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: 21:b9:05:1d:0a:d1:e1:58 W@08:54:51.479 spec-protocol> Aug 25, 2026 8:54:54 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@08:54:54.660 spec-protocol> PASS #1: TypeCheckerSnowcat I@08:54:55.261 spec-protocol> > Running Snowcat .::. I@08:54:55.261 spec-protocol> > Your types are purrfect! I@08:54:57.259 spec-protocol> > All expressions are typed I@08:54:57.260 spec-protocol> PASS #2: ConfigurationPass I@08:54:57.261 spec-protocol> > Set the initialization predicate to q::init I@08:54:57.267 spec-protocol> > Set the transition predicate to q::step I@08:54:57.267 spec-protocol> > Set an invariant to q::inductiveInv I@08:54:57.267 spec-protocol> PASS #3: DesugarerPass I@08:54:57.274 spec-protocol> > Desugaring... I@08:54:57.274 spec-protocol> PASS #4: InlinePass I@08:54:57.290 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@08:54:57.290 spec-protocol> PASS #5: TemporalPass I@08:54:57.384 spec-protocol> > Rewriting temporal operators... I@08:54:57.384 spec-protocol> > No temporal property specified, nothing to encode I@08:54:57.384 spec-protocol> PASS #6: InlinePass I@08:54:57.384 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@08:54:57.384 spec-protocol> PASS #7: PrimingPass I@08:54:57.403 spec-protocol> > Introducing q::initPrimed for q::init' I@08:54:57.405 spec-protocol> PASS #8: VCGen I@08:54:57.406 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@08:54:57.406 spec-protocol> > VCGen produced 35 verification condition(s) I@08:54:57.415 spec-protocol> PASS #9: PreprocessingPass I@08:54:57.418 spec-protocol> > Before preprocessing: unique renaming I@08:54:57.418 spec-protocol> > Applying standard transformations: I@08:54:57.424 spec-protocol> > PrimePropagation I@08:54:57.424 spec-protocol> > Desugarer I@08:54:57.429 spec-protocol> > UniqueRenamer I@08:54:57.438 spec-protocol> > Normalizer I@08:54:57.457 spec-protocol> > Keramelizer I@08:54:57.472 spec-protocol> > After preprocessing: UniqueRenamer I@08:54:57.495 spec-protocol> PASS #10: TransitionFinderPass I@08:54:57.527 spec-protocol> > Found 1 initializing transitions I@08:54:57.540 spec-protocol> > Found 18 transitions I@08:54:57.568 spec-protocol> > No constant initializer I@08:54:57.569 spec-protocol> > Applying unique renaming I@08:54:57.570 spec-protocol> PASS #11: OptimizationPass I@08:54:57.590 spec-protocol> > Applying optimizations: I@08:54:57.597 spec-protocol> > ConstSimplifier I@08:54:57.598 spec-protocol> > ExprOptimizer I@08:54:57.650 spec-protocol> > SetMembershipSimplifier I@08:54:57.674 spec-protocol> > ConstSimplifier I@08:54:57.683 spec-protocol> PASS #12: AnalysisPass I@08:54:57.731 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@08:54:57.734 spec-protocol> > Skolemization I@08:54:57.734 spec-protocol> > Expansion I@08:54:57.739 spec-protocol> > Remove unused let-in defs I@08:54:57.754 spec-protocol> > Running analyzers... I@08:54:57.765 spec-protocol> > Introduced expression grades I@08:54:57.775 spec-protocol> PASS #13: BoundedChecker I@08:54:57.775 spec-protocol> State 0: Checking 35 state invariants I@08:54:58.170 spec-protocol> State 0: state invariant 0 holds. I@08:54:58.172 spec-protocol> State 0: state invariant 1 holds. I@08:54:58.213 spec-protocol> State 0: state invariant 2 holds. I@08:54:58.215 spec-protocol> State 0: state invariant 3 holds. I@08:54:58.217 spec-protocol> State 0: state invariant 4 holds. I@08:54:58.218 spec-protocol> State 0: state invariant 5 holds. I@08:54:58.227 spec-protocol> State 0: state invariant 6 holds. I@08:54:58.227 spec-protocol> State 0: state invariant 7 holds. I@08:54:58.228 spec-protocol> State 0: state invariant 8 holds. I@08:54:58.229 spec-protocol> State 0: state invariant 9 holds. I@08:54:58.238 spec-protocol> State 0: state invariant 10 holds. I@08:54:58.239 spec-protocol> State 0: state invariant 11 holds. I@08:54:58.240 spec-protocol> State 0: state invariant 12 holds. I@08:54:58.250 spec-protocol> State 0: state invariant 13 holds. I@08:54:58.250 spec-protocol> State 0: state invariant 14 holds. I@08:54:58.255 spec-protocol> State 0: state invariant 15 holds. I@08:54:58.259 spec-protocol> State 0: state invariant 16 holds. I@08:54:58.264 spec-protocol> State 0: state invariant 17 holds. I@08:54:58.274 spec-protocol> State 0: state invariant 18 holds. I@08:54:58.279 spec-protocol> State 0: state invariant 19 holds. I@08:54:58.282 spec-protocol> State 0: state invariant 20 holds. I@08:54:58.283 spec-protocol> State 0: state invariant 21 holds. I@08:54:58.288 spec-protocol> State 0: state invariant 22 holds. I@08:54:58.297 spec-protocol> State 0: state invariant 23 holds. I@08:54:58.304 spec-protocol> State 0: state invariant 24 holds. I@08:54:58.362 spec-protocol> State 0: state invariant 25 holds. I@08:54:58.370 spec-protocol> State 0: state invariant 26 holds. I@08:54:58.392 spec-protocol> State 0: state invariant 27 holds. I@08:54:58.420 spec-protocol> State 0: state invariant 28 holds. I@08:54:58.448 spec-protocol> State 0: state invariant 29 holds. I@08:54:58.449 spec-protocol> State 0: state invariant 30 holds. I@08:54:58.461 spec-protocol> State 0: state invariant 31 holds. I@08:54:58.472 spec-protocol> State 0: state invariant 32 holds. I@08:54:58.473 spec-protocol> State 0: state invariant 33 holds. I@08:54:58.474 spec-protocol> State 0: state invariant 34 holds. I@08:54:58.475 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@08:54:58.475 spec-protocol> The outcome is: NoError I@08:54:58.491 spec-protocol> > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... spec-protocol> PASS #0: SanyParser I@08:54:58.840 spec-protocol> PASS #1: TypeCheckerSnowcat I@08:54:58.941 spec-protocol> > Running Snowcat .::. I@08:54:58.941 spec-protocol> > Your types are purrfect! I@08:55:00.778 spec-protocol> > All expressions are typed I@08:55:00.779 spec-protocol> PASS #2: ConfigurationPass I@08:55:00.779 spec-protocol> > Set the initialization predicate to q::inductiveInv I@08:55:00.779 spec-protocol> > Set the transition predicate to q::step I@08:55:00.780 spec-protocol> > Set an invariant to q::inductiveInv I@08:55:00.780 spec-protocol> PASS #3: DesugarerPass I@08:55:00.781 spec-protocol> > Desugaring... I@08:55:00.782 spec-protocol> PASS #4: InlinePass I@08:55:00.784 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@08:55:00.784 spec-protocol> PASS #5: TemporalPass I@08:55:00.811 spec-protocol> > Rewriting temporal operators... I@08:55:00.811 spec-protocol> > No temporal property specified, nothing to encode I@08:55:00.811 spec-protocol> PASS #6: InlinePass I@08:55:00.811 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@08:55:00.811 spec-protocol> PASS #7: PrimingPass I@08:55:00.821 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@08:55:00.821 spec-protocol> PASS #8: VCGen I@08:55:00.822 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@08:55:00.823 spec-protocol> > VCGen produced 35 verification condition(s) I@08:55:00.823 spec-protocol> PASS #9: PreprocessingPass I@08:55:00.824 spec-protocol> > Before preprocessing: unique renaming I@08:55:00.824 spec-protocol> > Applying standard transformations: I@08:55:00.824 spec-protocol> > PrimePropagation I@08:55:00.824 spec-protocol> > Desugarer I@08:55:00.828 spec-protocol> > UniqueRenamer I@08:55:00.834 spec-protocol> > Normalizer I@08:55:00.843 spec-protocol> > Keramelizer I@08:55:00.857 spec-protocol> > After preprocessing: UniqueRenamer I@08:55:00.868 spec-protocol> PASS #10: TransitionFinderPass I@08:55:00.880 spec-protocol> > Found 1 initializing transitions I@08:55:00.883 spec-protocol> > Found 18 transitions I@08:55:00.892 spec-protocol> > No constant initializer I@08:55:00.892 spec-protocol> > Applying unique renaming I@08:55:00.893 spec-protocol> PASS #11: OptimizationPass I@08:55:00.910 spec-protocol> > Applying optimizations: I@08:55:00.910 spec-protocol> > ConstSimplifier I@08:55:00.911 spec-protocol> > ExprOptimizer I@08:55:00.971 spec-protocol> > SetMembershipSimplifier I@08:55:00.984 spec-protocol> > ConstSimplifier I@08:55:00.988 spec-protocol> PASS #12: AnalysisPass I@08:55:01.043 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@08:55:01.043 spec-protocol> > Skolemization I@08:55:01.043 spec-protocol> > Expansion I@08:55:01.046 spec-protocol> > Remove unused let-in defs I@08:55:01.054 spec-protocol> > Running analyzers... I@08:55:01.057 spec-protocol> > Introduced expression grades I@08:55:01.059 spec-protocol> PASS #13: BoundedChecker I@08:55:01.060 spec-protocol> State 0: Checking 35 state invariants I@08:55:01.557 spec-protocol> State 0: state invariant 0 holds. I@08:55:01.558 spec-protocol> State 0: state invariant 1 holds. I@08:55:01.576 spec-protocol> State 0: state invariant 2 holds. I@08:55:01.578 spec-protocol> State 0: state invariant 3 holds. I@08:55:01.579 spec-protocol> State 0: state invariant 4 holds. I@08:55:01.580 spec-protocol> State 0: state invariant 5 holds. I@08:55:01.584 spec-protocol> State 0: state invariant 6 holds. I@08:55:01.585 spec-protocol> State 0: state invariant 7 holds. I@08:55:01.586 spec-protocol> State 0: state invariant 8 holds. I@08:55:01.588 spec-protocol> State 0: state invariant 9 holds. I@08:55:01.595 spec-protocol> State 0: state invariant 10 holds. I@08:55:01.596 spec-protocol> State 0: state invariant 11 holds. I@08:55:01.597 spec-protocol> State 0: state invariant 12 holds. I@08:55:01.603 spec-protocol> State 0: state invariant 13 holds. I@08:55:01.605 spec-protocol> State 0: state invariant 14 holds. I@08:55:01.609 spec-protocol> State 0: state invariant 15 holds. I@08:55:01.615 spec-protocol> State 0: state invariant 16 holds. I@08:55:01.626 spec-protocol> State 0: state invariant 17 holds. I@08:55:01.637 spec-protocol> State 0: state invariant 18 holds. I@08:55:01.646 spec-protocol> State 0: state invariant 19 holds. I@08:55:01.647 spec-protocol> State 0: state invariant 20 holds. I@08:55:01.647 spec-protocol> State 0: state invariant 21 holds. I@08:55:01.648 spec-protocol> State 0: state invariant 22 holds. I@08:55:01.653 spec-protocol> State 0: state invariant 23 holds. I@08:55:01.660 spec-protocol> State 0: state invariant 24 holds. I@08:55:01.716 spec-protocol> State 0: state invariant 25 holds. I@08:55:01.722 spec-protocol> State 0: state invariant 26 holds. I@08:55:01.824 spec-protocol> State 0: state invariant 27 holds. I@08:55:01.890 spec-protocol> State 0: state invariant 28 holds. I@08:55:02.014 spec-protocol> State 0: state invariant 29 holds. I@08:55:02.017 spec-protocol> State 0: state invariant 30 holds. I@08:55:02.030 spec-protocol> State 0: state invariant 31 holds. I@08:55:02.045 spec-protocol> State 0: state invariant 32 holds. I@08:55:02.046 spec-protocol> State 0: state invariant 33 holds. I@08:55:02.047 spec-protocol> State 0: state invariant 34 holds. I@08:55:02.048 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@08:55:02.048 spec-protocol> State 1: Checking 4 state invariants I@08:55:02.061 spec-protocol> State 1: state invariant 8 holds. I@08:55:02.062 spec-protocol> State 1: state invariant 25 holds. I@08:55:02.067 spec-protocol> State 1: state invariant 26 holds. I@08:55:02.180 spec-protocol> State 1: state invariant 27 holds. I@08:55:02.249 spec-protocol> State 1: Checking 15 state invariants I@08:55:02.264 spec-protocol> State 1: state invariant 0 holds. I@08:55:02.265 spec-protocol> State 1: state invariant 1 holds. I@08:55:02.282 spec-protocol> State 1: state invariant 12 holds. I@08:55:02.290 spec-protocol> State 1: state invariant 14 holds. I@08:55:02.297 spec-protocol> State 1: state invariant 15 holds. I@08:55:02.303 spec-protocol> State 1: state invariant 16 holds. I@08:55:02.310 spec-protocol> State 1: state invariant 17 holds. I@08:55:02.321 spec-protocol> State 1: state invariant 22 holds. I@08:55:02.329 spec-protocol> State 1: state invariant 24 holds. I@08:55:02.380 spec-protocol> State 1: state invariant 25 holds. I@08:55:02.387 spec-protocol> State 1: state invariant 26 holds. I@08:55:02.472 spec-protocol> State 1: state invariant 27 holds. I@08:55:02.544 spec-protocol> State 1: state invariant 28 holds. I@08:55:02.627 spec-protocol> State 1: state invariant 33 holds. I@08:55:02.630 spec-protocol> State 1: state invariant 34 holds. I@08:55:02.631 spec-protocol> State 1: Checking 18 state invariants I@08:55:02.773 spec-protocol> State 1: state invariant 5 holds. I@08:55:02.777 spec-protocol> State 1: state invariant 6 holds. I@08:55:02.779 spec-protocol> State 1: state invariant 7 holds. I@08:55:02.780 spec-protocol> State 1: state invariant 9 holds. I@08:55:02.786 spec-protocol> State 1: state invariant 10 holds. I@08:55:02.787 spec-protocol> State 1: state invariant 13 holds. I@08:55:02.788 spec-protocol> State 1: state invariant 18 holds. I@08:55:02.797 spec-protocol> State 1: state invariant 19 holds. I@08:55:02.799 spec-protocol> State 1: state invariant 21 holds. I@08:55:02.801 spec-protocol> State 1: state invariant 22 holds. I@08:55:02.809 spec-protocol> State 1: state invariant 24 holds. I@08:55:02.849 spec-protocol> State 1: state invariant 25 holds. I@08:55:02.856 spec-protocol> State 1: state invariant 26 holds. I@08:55:02.903 spec-protocol> State 1: state invariant 27 holds. I@08:55:02.938 spec-protocol> State 1: state invariant 28 holds. I@08:55:03.002 spec-protocol> State 1: state invariant 29 holds. I@08:55:03.005 spec-protocol> State 1: state invariant 30 holds. I@08:55:03.018 spec-protocol> State 1: state invariant 31 holds. I@08:55:03.057 spec-protocol> State 1: Checking 14 state invariants I@08:55:03.169 spec-protocol> State 1: state invariant 5 holds. I@08:55:03.172 spec-protocol> State 1: state invariant 6 holds. I@08:55:03.174 spec-protocol> State 1: state invariant 7 holds. I@08:55:03.175 spec-protocol> State 1: state invariant 9 holds. I@08:55:03.181 spec-protocol> State 1: state invariant 10 holds. I@08:55:03.183 spec-protocol> State 1: state invariant 13 holds. I@08:55:03.184 spec-protocol> State 1: state invariant 19 holds. I@08:55:03.185 spec-protocol> State 1: state invariant 21 holds. I@08:55:03.187 spec-protocol> State 1: state invariant 22 holds. I@08:55:03.192 spec-protocol> State 1: state invariant 24 holds. I@08:55:03.212 spec-protocol> State 1: state invariant 25 holds. I@08:55:03.218 spec-protocol> State 1: state invariant 26 holds. I@08:55:03.262 spec-protocol> State 1: state invariant 27 holds. I@08:55:03.295 spec-protocol> State 1: state invariant 28 holds. I@08:55:03.338 spec-protocol> State 1: Checking 26 state invariants I@08:55:03.434 spec-protocol> State 1: state invariant 0 holds. I@08:55:03.435 spec-protocol> State 1: state invariant 1 holds. I@08:55:03.454 spec-protocol> State 1: state invariant 5 holds. I@08:55:03.459 spec-protocol> State 1: state invariant 6 holds. I@08:55:03.460 spec-protocol> State 1: state invariant 7 holds. I@08:55:03.462 spec-protocol> State 1: state invariant 9 holds. I@08:55:03.469 spec-protocol> State 1: state invariant 10 holds. I@08:55:03.480 spec-protocol> State 1: state invariant 12 holds. I@08:55:03.487 spec-protocol> State 1: state invariant 13 holds. I@08:55:03.488 spec-protocol> State 1: state invariant 14 holds. I@08:55:03.497 spec-protocol> State 1: state invariant 15 holds. I@08:55:03.504 spec-protocol> State 1: state invariant 16 holds. I@08:55:03.509 spec-protocol> State 1: state invariant 17 holds. I@08:55:03.519 spec-protocol> State 1: state invariant 18 holds. I@08:55:03.539 spec-protocol> State 1: state invariant 19 holds. I@08:55:03.541 spec-protocol> State 1: state invariant 21 holds. I@08:55:03.544 spec-protocol> State 1: state invariant 22 holds. I@08:55:03.564 spec-protocol> State 1: state invariant 23 holds. I@08:55:03.571 spec-protocol> State 1: state invariant 24 holds. I@08:55:03.643 spec-protocol> State 1: state invariant 25 holds. I@08:55:03.650 spec-protocol> State 1: state invariant 26 holds. I@08:55:03.738 spec-protocol> State 1: state invariant 27 holds. I@08:55:03.804 spec-protocol> State 1: state invariant 28 holds. I@08:55:04.075 spec-protocol> State 1: state invariant 29 holds. I@08:55:04.079 spec-protocol> State 1: state invariant 30 holds. I@08:55:04.094 spec-protocol> State 1: state invariant 31 holds. I@08:55:04.143 spec-protocol> State 1: Checking 22 state invariants I@08:55:04.243 spec-protocol> State 1: state invariant 0 holds. I@08:55:04.244 spec-protocol> State 1: state invariant 1 holds. I@08:55:04.262 spec-protocol> State 1: state invariant 5 holds. I@08:55:04.268 spec-protocol> State 1: state invariant 6 holds. I@08:55:04.269 spec-protocol> State 1: state invariant 7 holds. I@08:55:04.270 spec-protocol> State 1: state invariant 9 holds. I@08:55:04.278 spec-protocol> State 1: state invariant 10 holds. I@08:55:04.282 spec-protocol> State 1: state invariant 12 holds. I@08:55:04.287 spec-protocol> State 1: state invariant 13 holds. I@08:55:04.289 spec-protocol> State 1: state invariant 14 holds. I@08:55:04.295 spec-protocol> State 1: state invariant 15 holds. I@08:55:04.303 spec-protocol> State 1: state invariant 16 holds. I@08:55:04.311 spec-protocol> State 1: state invariant 17 holds. I@08:55:04.325 spec-protocol> State 1: state invariant 19 holds. I@08:55:04.326 spec-protocol> State 1: state invariant 21 holds. I@08:55:04.330 spec-protocol> State 1: state invariant 22 holds. I@08:55:04.340 spec-protocol> State 1: state invariant 23 holds. I@08:55:04.347 spec-protocol> State 1: state invariant 24 holds. I@08:55:04.394 spec-protocol> State 1: state invariant 25 holds. I@08:55:04.401 spec-protocol> State 1: state invariant 26 holds. I@08:55:04.519 spec-protocol> State 1: state invariant 27 holds. I@08:55:04.587 spec-protocol> State 1: state invariant 28 holds. I@08:55:04.670 spec-protocol> Step 1: Transition #6 is disabled I@08:55:04.706 spec-protocol> Step 1: Transition #7 is disabled I@08:55:04.735 spec-protocol> State 1: Checking 27 state invariants I@08:55:04.826 spec-protocol> State 1: state invariant 0 holds. I@08:55:04.827 spec-protocol> State 1: state invariant 1 holds. I@08:55:04.840 spec-protocol> State 1: state invariant 5 holds. I@08:55:04.847 spec-protocol> State 1: state invariant 6 holds. I@08:55:04.849 spec-protocol> State 1: state invariant 8 holds. I@08:55:04.850 spec-protocol> State 1: state invariant 9 holds. I@08:55:04.855 spec-protocol> State 1: state invariant 10 holds. I@08:55:04.859 spec-protocol> State 1: state invariant 11 holds. I@08:55:04.860 spec-protocol> State 1: state invariant 12 holds. I@08:55:04.865 spec-protocol> State 1: state invariant 13 holds. I@08:55:04.866 spec-protocol> State 1: state invariant 14 holds. I@08:55:04.870 spec-protocol> State 1: state invariant 15 holds. I@08:55:04.884 spec-protocol> State 1: state invariant 16 holds. I@08:55:04.889 spec-protocol> State 1: state invariant 17 holds. I@08:55:04.897 spec-protocol> State 1: state invariant 18 holds. I@08:55:04.915 spec-protocol> State 1: state invariant 19 holds. I@08:55:04.917 spec-protocol> State 1: state invariant 21 holds. I@08:55:04.919 spec-protocol> State 1: state invariant 22 holds. I@08:55:04.931 spec-protocol> State 1: state invariant 23 holds. I@08:55:04.938 spec-protocol> State 1: state invariant 24 holds. I@08:55:04.988 spec-protocol> State 1: state invariant 25 holds. I@08:55:04.995 spec-protocol> State 1: state invariant 26 holds. I@08:55:05.080 spec-protocol> State 1: state invariant 27 holds. I@08:55:05.150 spec-protocol> State 1: state invariant 28 holds. I@08:55:05.265 spec-protocol> State 1: state invariant 29 holds. I@08:55:05.268 spec-protocol> State 1: state invariant 30 holds. I@08:55:05.287 spec-protocol> State 1: state invariant 31 holds. I@08:55:05.332 spec-protocol> State 1: Checking 23 state invariants I@08:55:05.418 spec-protocol> State 1: state invariant 0 holds. I@08:55:05.419 spec-protocol> State 1: state invariant 1 holds. I@08:55:05.434 spec-protocol> State 1: state invariant 5 holds. I@08:55:05.440 spec-protocol> State 1: state invariant 6 holds. I@08:55:05.441 spec-protocol> State 1: state invariant 8 holds. I@08:55:05.443 spec-protocol> State 1: state invariant 9 holds. I@08:55:05.448 spec-protocol> State 1: state invariant 10 holds. I@08:55:05.453 spec-protocol> State 1: state invariant 11 holds. I@08:55:05.454 spec-protocol> State 1: state invariant 12 holds. I@08:55:05.458 spec-protocol> State 1: state invariant 13 holds. I@08:55:05.459 spec-protocol> State 1: state invariant 14 holds. I@08:55:05.464 spec-protocol> State 1: state invariant 15 holds. I@08:55:05.471 spec-protocol> State 1: state invariant 16 holds. I@08:55:05.478 spec-protocol> State 1: state invariant 17 holds. I@08:55:05.486 spec-protocol> State 1: state invariant 19 holds. I@08:55:05.488 spec-protocol> State 1: state invariant 21 holds. I@08:55:05.491 spec-protocol> State 1: state invariant 22 holds. I@08:55:05.498 spec-protocol> State 1: state invariant 23 holds. I@08:55:05.505 spec-protocol> State 1: state invariant 24 holds. I@08:55:05.538 spec-protocol> State 1: state invariant 25 holds. I@08:55:05.545 spec-protocol> State 1: state invariant 26 holds. I@08:55:05.656 spec-protocol> State 1: state invariant 27 holds. I@08:55:05.719 spec-protocol> State 1: state invariant 28 holds. I@08:55:05.808 spec-protocol> State 1: Checking 26 state invariants I@08:55:05.977 spec-protocol> State 1: state invariant 0 holds. I@08:55:05.979 spec-protocol> State 1: state invariant 1 holds. I@08:55:05.995 spec-protocol> State 1: state invariant 5 holds. I@08:55:06.004 spec-protocol> State 1: state invariant 6 holds. I@08:55:06.005 spec-protocol> State 1: state invariant 9 holds. I@08:55:06.011 spec-protocol> State 1: state invariant 10 holds. I@08:55:06.014 spec-protocol> State 1: state invariant 11 holds. I@08:55:06.015 spec-protocol> State 1: state invariant 12 holds. I@08:55:06.020 spec-protocol> State 1: state invariant 13 holds. I@08:55:06.021 spec-protocol> State 1: state invariant 14 holds. I@08:55:06.038 spec-protocol> State 1: state invariant 15 holds. I@08:55:06.046 spec-protocol> State 1: state invariant 16 holds. I@08:55:06.053 spec-protocol> State 1: state invariant 17 holds. I@08:55:06.068 spec-protocol> State 1: state invariant 18 holds. I@08:55:06.086 spec-protocol> State 1: state invariant 19 holds. I@08:55:06.088 spec-protocol> State 1: state invariant 21 holds. I@08:55:06.092 spec-protocol> State 1: state invariant 22 holds. I@08:55:06.103 spec-protocol> State 1: state invariant 23 holds. I@08:55:06.110 spec-protocol> State 1: state invariant 24 holds. I@08:55:06.152 spec-protocol> State 1: state invariant 25 holds. I@08:55:06.159 spec-protocol> State 1: state invariant 26 holds. I@08:55:06.240 spec-protocol> State 1: state invariant 27 holds. I@08:55:06.290 spec-protocol> State 1: state invariant 28 holds. I@08:55:06.359 spec-protocol> State 1: state invariant 29 holds. I@08:55:06.362 spec-protocol> State 1: state invariant 30 holds. I@08:55:06.376 spec-protocol> State 1: state invariant 31 holds. I@08:55:06.425 spec-protocol> State 1: Checking 22 state invariants I@08:55:06.570 spec-protocol> State 1: state invariant 0 holds. I@08:55:06.572 spec-protocol> State 1: state invariant 1 holds. I@08:55:06.588 spec-protocol> State 1: state invariant 5 holds. I@08:55:06.595 spec-protocol> State 1: state invariant 6 holds. I@08:55:06.596 spec-protocol> State 1: state invariant 9 holds. I@08:55:06.602 spec-protocol> State 1: state invariant 10 holds. I@08:55:06.608 spec-protocol> State 1: state invariant 11 holds. I@08:55:06.609 spec-protocol> State 1: state invariant 12 holds. I@08:55:06.616 spec-protocol> State 1: state invariant 13 holds. I@08:55:06.617 spec-protocol> State 1: state invariant 14 holds. I@08:55:06.626 spec-protocol> State 1: state invariant 15 holds. I@08:55:06.630 spec-protocol> State 1: state invariant 16 holds. I@08:55:06.641 spec-protocol> State 1: state invariant 17 holds. I@08:55:06.650 spec-protocol> State 1: state invariant 19 holds. I@08:55:06.652 spec-protocol> State 1: state invariant 21 holds. I@08:55:06.655 spec-protocol> State 1: state invariant 22 holds. I@08:55:06.667 spec-protocol> State 1: state invariant 23 holds. I@08:55:06.674 spec-protocol> State 1: state invariant 24 holds. I@08:55:06.696 spec-protocol> State 1: state invariant 25 holds. I@08:55:06.703 spec-protocol> State 1: state invariant 26 holds. I@08:55:06.783 spec-protocol> State 1: state invariant 27 holds. I@08:55:06.834 spec-protocol> State 1: state invariant 28 holds. I@08:55:06.900 spec-protocol> Step 1: Transition #12 is disabled I@08:55:06.935 spec-protocol> State 1: Checking 21 state invariants I@08:55:06.981 spec-protocol> State 1: state invariant 0 holds. I@08:55:06.982 spec-protocol> State 1: state invariant 1 holds. I@08:55:06.999 spec-protocol> State 1: state invariant 5 holds. I@08:55:07.005 spec-protocol> State 1: state invariant 6 holds. I@08:55:07.007 spec-protocol> State 1: state invariant 9 holds. I@08:55:07.013 spec-protocol> State 1: state invariant 10 holds. I@08:55:07.020 spec-protocol> State 1: state invariant 12 holds. I@08:55:07.026 spec-protocol> State 1: state invariant 13 holds. I@08:55:07.027 spec-protocol> State 1: state invariant 14 holds. I@08:55:07.040 spec-protocol> State 1: state invariant 15 holds. I@08:55:07.056 spec-protocol> State 1: state invariant 16 holds. I@08:55:07.065 spec-protocol> State 1: state invariant 17 holds. I@08:55:07.085 spec-protocol> State 1: state invariant 19 holds. I@08:55:07.088 spec-protocol> State 1: state invariant 21 holds. I@08:55:07.090 spec-protocol> State 1: state invariant 22 holds. I@08:55:07.102 spec-protocol> State 1: state invariant 23 holds. I@08:55:07.110 spec-protocol> State 1: state invariant 24 holds. I@08:55:07.160 spec-protocol> State 1: state invariant 25 holds. I@08:55:07.168 spec-protocol> State 1: state invariant 26 holds. I@08:55:07.309 spec-protocol> State 1: state invariant 27 holds. I@08:55:07.389 spec-protocol> State 1: state invariant 28 holds. I@08:55:07.520 spec-protocol> Step 1: Transition #14 is disabled I@08:55:07.554 spec-protocol> Step 1: Transition #15 is disabled I@08:55:07.609 spec-protocol> State 1: Checking 14 state invariants I@08:55:07.670 spec-protocol> State 1: state invariant 2 holds. I@08:55:07.670 spec-protocol> State 1: state invariant 3 holds. I@08:55:07.673 spec-protocol> State 1: state invariant 18 holds. I@08:55:07.687 spec-protocol> State 1: state invariant 20 holds. I@08:55:07.691 spec-protocol> State 1: state invariant 22 holds. I@08:55:07.705 spec-protocol> State 1: state invariant 24 holds. I@08:55:07.738 spec-protocol> State 1: state invariant 25 holds. I@08:55:07.744 spec-protocol> State 1: state invariant 26 holds. I@08:55:07.833 spec-protocol> State 1: state invariant 27 holds. I@08:55:07.871 spec-protocol> State 1: state invariant 28 holds. I@08:55:07.915 spec-protocol> State 1: state invariant 29 holds. I@08:55:07.919 spec-protocol> State 1: state invariant 30 holds. I@08:55:07.930 spec-protocol> State 1: state invariant 31 holds. I@08:55:07.944 spec-protocol> State 1: state invariant 34 holds. I@08:55:07.946 spec-protocol> State 1: Checking 21 state invariants I@08:55:08.016 spec-protocol> State 1: state invariant 0 holds. I@08:55:08.018 spec-protocol> State 1: state invariant 1 holds. I@08:55:08.036 spec-protocol> State 1: state invariant 2 holds. I@08:55:08.037 spec-protocol> State 1: state invariant 3 holds. I@08:55:08.038 spec-protocol> State 1: state invariant 14 holds. I@08:55:08.049 spec-protocol> State 1: state invariant 15 holds. I@08:55:08.055 spec-protocol> State 1: state invariant 16 holds. I@08:55:08.061 spec-protocol> State 1: state invariant 17 holds. I@08:55:08.076 spec-protocol> State 1: state invariant 18 holds. I@08:55:08.090 spec-protocol> State 1: state invariant 20 holds. I@08:55:08.091 spec-protocol> State 1: state invariant 22 holds. I@08:55:08.096 spec-protocol> State 1: state invariant 23 holds. I@08:55:08.104 spec-protocol> State 1: state invariant 24 holds. I@08:55:08.146 spec-protocol> State 1: state invariant 25 holds. I@08:55:08.152 spec-protocol> State 1: state invariant 26 holds. I@08:55:08.294 spec-protocol> State 1: state invariant 27 holds. I@08:55:08.352 spec-protocol> State 1: state invariant 28 holds. I@08:55:08.437 spec-protocol> State 1: state invariant 29 holds. I@08:55:08.441 spec-protocol> State 1: state invariant 30 holds. I@08:55:08.454 spec-protocol> State 1: state invariant 31 holds. I@08:55:08.468 spec-protocol> State 1: state invariant 34 holds. I@08:55:08.469 spec-protocol> Step 1: picking a transition out of 13 transition(s) I@08:55:08.471 spec-protocol> The outcome is: NoError I@08:55:08.617 spec-protocol> > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... spec-protocol> PASS #0: SanyParser I@08:55:08.749 spec-protocol> PASS #1: TypeCheckerSnowcat I@08:55:08.809 spec-protocol> > Running Snowcat .::. I@08:55:08.809 spec-protocol> > Your types are purrfect! I@08:55:10.272 spec-protocol> > All expressions are typed I@08:55:10.273 spec-protocol> PASS #2: ConfigurationPass I@08:55:10.273 spec-protocol> > Set the initialization predicate to q::inductiveInv I@08:55:10.274 spec-protocol> > Set the transition predicate to q::step I@08:55:10.274 spec-protocol> > Set an invariant to q::inv I@08:55:10.274 spec-protocol> PASS #3: DesugarerPass I@08:55:10.276 spec-protocol> > Desugaring... I@08:55:10.276 spec-protocol> PASS #4: InlinePass I@08:55:10.277 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@08:55:10.277 spec-protocol> PASS #5: TemporalPass I@08:55:10.316 spec-protocol> > Rewriting temporal operators... I@08:55:10.316 spec-protocol> > No temporal property specified, nothing to encode I@08:55:10.316 spec-protocol> PASS #6: InlinePass I@08:55:10.316 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@08:55:10.316 spec-protocol> PASS #7: PrimingPass I@08:55:10.332 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@08:55:10.332 spec-protocol> PASS #8: VCGen I@08:55:10.333 spec-protocol> > Producing verification conditions from the invariant q::inv I@08:55:10.333 spec-protocol> > VCGen produced 5 verification condition(s) I@08:55:10.334 spec-protocol> PASS #9: PreprocessingPass I@08:55:10.334 spec-protocol> > Before preprocessing: unique renaming I@08:55:10.334 spec-protocol> > Applying standard transformations: I@08:55:10.334 spec-protocol> > PrimePropagation I@08:55:10.334 spec-protocol> > Desugarer I@08:55:10.337 spec-protocol> > UniqueRenamer I@08:55:10.342 spec-protocol> > Normalizer I@08:55:10.358 spec-protocol> > Keramelizer I@08:55:10.364 spec-protocol> > After preprocessing: UniqueRenamer I@08:55:10.374 spec-protocol> PASS #10: TransitionFinderPass I@08:55:10.393 spec-protocol> > Found 1 initializing transitions I@08:55:10.395 spec-protocol> > Found 18 transitions I@08:55:10.404 spec-protocol> > No constant initializer I@08:55:10.404 spec-protocol> > Applying unique renaming I@08:55:10.404 spec-protocol> PASS #11: OptimizationPass I@08:55:10.429 spec-protocol> > Applying optimizations: I@08:55:10.429 spec-protocol> > ConstSimplifier I@08:55:10.429 spec-protocol> > ExprOptimizer I@08:55:10.472 spec-protocol> > SetMembershipSimplifier I@08:55:10.480 spec-protocol> > ConstSimplifier I@08:55:10.485 spec-protocol> PASS #12: AnalysisPass I@08:55:10.526 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@08:55:10.526 spec-protocol> > Skolemization I@08:55:10.526 spec-protocol> > Expansion I@08:55:10.530 spec-protocol> > Remove unused let-in defs I@08:55:10.536 spec-protocol> > Running analyzers... I@08:55:10.540 spec-protocol> > Introduced expression grades I@08:55:10.540 spec-protocol> PASS #13: BoundedChecker I@08:55:10.540 spec-protocol> State 0: Checking 5 state invariants I@08:55:10.921 spec-protocol> State 0: state invariant 0 holds. I@08:55:10.922 spec-protocol> State 0: state invariant 1 holds. I@08:55:10.923 spec-protocol> State 0: state invariant 2 holds. I@08:55:10.924 spec-protocol> State 0: state invariant 3 holds. I@08:55:10.928 spec-protocol> State 0: state invariant 4 holds. I@08:55:10.984 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@08:55:10.987 spec-protocol> The outcome is: NoError I@08:55:10.997 spec-protocol> [ok] No violation found (20955ms). 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