this derivation will be built: /nix/store/3m8byqyx151gm2p36ygm2mg4p8k32jy6-spec-protocol.drv these 2 paths will be fetched (211.6 MiB download, 342.5 MiB unpacked): /nix/store/6qjq3nq0lkml1fzhcldnfrid38c3xp41-quint-0.33.0 /nix/store/l1d4l5z14wiw8ns3pgv59szb01206gcf-quint-cli-0.33.0 building '/nix/store/3m8byqyx151gm2p36ygm2mg4p8k32jy6-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-10-18T16-53-52_3792579933075861651 spec-protocol> # APALACHE version: 0.62.1 | build: a321771 I@16:53:52.395 spec-protocol> Starting checker server on port 8822... I@16:53:52.399 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: b9:9f:b8:39:a6:c8:cd:4b W@16:53:53.093 spec-protocol> Oct 18, 2026 4:53:56 PM 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@16:53:57.535 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:53:58.294 spec-protocol> > Running Snowcat .::. I@16:53:58.294 spec-protocol> > Your types are purrfect! I@16:54:00.664 spec-protocol> > All expressions are typed I@16:54:00.666 spec-protocol> PASS #2: ConfigurationPass I@16:54:00.668 spec-protocol> > Set the initialization predicate to q::init I@16:54:00.673 spec-protocol> > Set the transition predicate to q::step I@16:54:00.674 spec-protocol> > Set an invariant to q::inductiveInv I@16:54:00.674 spec-protocol> PASS #3: DesugarerPass I@16:54:00.682 spec-protocol> > Desugaring... I@16:54:00.682 spec-protocol> PASS #4: InlinePass I@16:54:00.700 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:00.701 spec-protocol> PASS #5: TemporalPass I@16:54:00.813 spec-protocol> > Rewriting temporal operators... I@16:54:00.814 spec-protocol> > No temporal property specified, nothing to encode I@16:54:00.814 spec-protocol> PASS #6: InlinePass I@16:54:00.814 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:00.814 spec-protocol> PASS #7: PrimingPass I@16:54:00.841 spec-protocol> > Introducing q::initPrimed for q::init' I@16:54:00.844 spec-protocol> PASS #8: VCGen I@16:54:00.845 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@16:54:00.846 spec-protocol> > VCGen produced 39 verification condition(s) I@16:54:00.855 spec-protocol> PASS #9: PreprocessingPass I@16:54:00.861 spec-protocol> > Before preprocessing: unique renaming I@16:54:00.861 spec-protocol> > Applying standard transformations: I@16:54:00.868 spec-protocol> > PrimePropagation I@16:54:00.869 spec-protocol> > Desugarer I@16:54:00.879 spec-protocol> > UniqueRenamer I@16:54:00.887 spec-protocol> > Normalizer I@16:54:00.914 spec-protocol> > SetMembershipSimplifier I@16:54:00.936 spec-protocol> > Keramelizer I@16:54:00.947 spec-protocol> > After preprocessing: UniqueRenamer I@16:54:00.972 spec-protocol> PASS #10: TransitionFinderPass I@16:54:01.019 spec-protocol> > Found 1 initializing transitions I@16:54:01.033 spec-protocol> > Found 24 transitions I@16:54:01.071 spec-protocol> > No constant initializer I@16:54:01.072 spec-protocol> > Applying unique renaming I@16:54:01.074 spec-protocol> PASS #11: OptimizationPass I@16:54:01.106 spec-protocol> > Applying optimizations: I@16:54:01.111 spec-protocol> > ConstSimplifier I@16:54:01.112 spec-protocol> > ExprOptimizer I@16:54:01.192 spec-protocol> > SetMembershipSimplifier I@16:54:01.217 spec-protocol> > ConstSimplifier I@16:54:01.224 spec-protocol> PASS #12: AnalysisPass I@16:54:01.297 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:54:01.301 spec-protocol> > Skolemization I@16:54:01.301 spec-protocol> > Expansion I@16:54:01.306 spec-protocol> > Remove unused let-in defs I@16:54:01.325 spec-protocol> > Running analyzers... I@16:54:01.337 spec-protocol> > Introduced expression grades I@16:54:01.347 spec-protocol> PASS #13: BoundedChecker I@16:54:01.348 spec-protocol> State 0: Checking 39 state invariants I@16:54:01.820 spec-protocol> State 0: state invariant 0 holds. I@16:54:01.826 spec-protocol> State 0: state invariant 1 holds. I@16:54:01.874 spec-protocol> State 0: state invariant 2 holds. I@16:54:01.875 spec-protocol> State 0: state invariant 3 holds. I@16:54:01.876 spec-protocol> State 0: state invariant 4 holds. I@16:54:01.906 spec-protocol> State 0: state invariant 5 holds. I@16:54:01.911 spec-protocol> State 0: state invariant 6 holds. I@16:54:01.913 spec-protocol> State 0: state invariant 7 holds. I@16:54:01.914 spec-protocol> State 0: state invariant 8 holds. I@16:54:01.915 spec-protocol> State 0: state invariant 9 holds. I@16:54:01.923 spec-protocol> State 0: state invariant 10 holds. I@16:54:01.924 spec-protocol> State 0: state invariant 11 holds. I@16:54:01.924 spec-protocol> State 0: state invariant 12 holds. I@16:54:01.935 spec-protocol> State 0: state invariant 13 holds. I@16:54:01.936 spec-protocol> State 0: state invariant 14 holds. I@16:54:01.944 spec-protocol> State 0: state invariant 15 holds. I@16:54:01.945 spec-protocol> State 0: state invariant 16 holds. I@16:54:01.945 spec-protocol> State 0: state invariant 17 holds. I@16:54:01.946 spec-protocol> State 0: state invariant 18 holds. I@16:54:01.948 spec-protocol> State 0: state invariant 19 holds. I@16:54:01.952 spec-protocol> State 0: state invariant 20 holds. I@16:54:01.957 spec-protocol> State 0: state invariant 21 holds. I@16:54:01.963 spec-protocol> State 0: state invariant 22 holds. I@16:54:01.967 spec-protocol> State 0: state invariant 23 holds. I@16:54:01.974 spec-protocol> State 0: state invariant 24 holds. I@16:54:01.977 spec-protocol> State 0: state invariant 25 holds. I@16:54:01.977 spec-protocol> State 0: state invariant 26 holds. I@16:54:01.982 spec-protocol> State 0: state invariant 27 holds. I@16:54:01.990 spec-protocol> State 0: state invariant 28 holds. I@16:54:02.006 spec-protocol> State 0: state invariant 29 holds. I@16:54:02.014 spec-protocol> State 0: state invariant 30 holds. I@16:54:02.036 spec-protocol> State 0: state invariant 31 holds. I@16:54:02.071 spec-protocol> State 0: state invariant 32 holds. I@16:54:02.098 spec-protocol> State 0: state invariant 33 holds. I@16:54:02.099 spec-protocol> State 0: state invariant 34 holds. I@16:54:02.104 spec-protocol> State 0: state invariant 35 holds. I@16:54:02.108 spec-protocol> State 0: state invariant 36 holds. I@16:54:02.109 spec-protocol> State 0: state invariant 37 holds. I@16:54:02.110 spec-protocol> State 0: state invariant 38 holds. I@16:54:02.110 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:54:02.111 spec-protocol> The outcome is: NoError I@16:54:02.119 spec-protocol> > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... spec-protocol> PASS #0: SanyParser I@16:54:02.492 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:54:02.694 spec-protocol> > Running Snowcat .::. I@16:54:02.694 spec-protocol> > Your types are purrfect! I@16:54:04.907 spec-protocol> > All expressions are typed I@16:54:04.908 spec-protocol> PASS #2: ConfigurationPass I@16:54:04.908 spec-protocol> > Set the initialization predicate to q::inductiveInv I@16:54:04.909 spec-protocol> > Set the transition predicate to q::step I@16:54:04.909 spec-protocol> > Set an invariant to q::inductiveInv I@16:54:04.909 spec-protocol> PASS #3: DesugarerPass I@16:54:04.911 spec-protocol> > Desugaring... I@16:54:04.911 spec-protocol> PASS #4: InlinePass I@16:54:04.913 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:04.913 spec-protocol> PASS #5: TemporalPass I@16:54:04.940 spec-protocol> > Rewriting temporal operators... I@16:54:04.940 spec-protocol> > No temporal property specified, nothing to encode I@16:54:04.940 spec-protocol> PASS #6: InlinePass I@16:54:04.941 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:04.941 spec-protocol> PASS #7: PrimingPass I@16:54:04.951 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:04.951 spec-protocol> PASS #8: VCGen I@16:54:04.952 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@16:54:04.952 spec-protocol> > VCGen produced 39 verification condition(s) I@16:54:04.953 spec-protocol> PASS #9: PreprocessingPass I@16:54:04.956 spec-protocol> > Before preprocessing: unique renaming I@16:54:04.956 spec-protocol> > Applying standard transformations: I@16:54:04.956 spec-protocol> > PrimePropagation I@16:54:04.956 spec-protocol> > Desugarer I@16:54:04.959 spec-protocol> > UniqueRenamer I@16:54:04.963 spec-protocol> > Normalizer I@16:54:04.973 spec-protocol> > SetMembershipSimplifier I@16:54:04.993 spec-protocol> > Keramelizer I@16:54:04.997 spec-protocol> > After preprocessing: UniqueRenamer I@16:54:05.007 spec-protocol> PASS #10: TransitionFinderPass I@16:54:05.023 spec-protocol> > Found 1 initializing transitions I@16:54:05.027 spec-protocol> > Found 24 transitions I@16:54:05.037 spec-protocol> > No constant initializer I@16:54:05.038 spec-protocol> > Applying unique renaming I@16:54:05.038 spec-protocol> PASS #11: OptimizationPass I@16:54:05.061 spec-protocol> > Applying optimizations: I@16:54:05.062 spec-protocol> > ConstSimplifier I@16:54:05.062 spec-protocol> > ExprOptimizer I@16:54:05.148 spec-protocol> > SetMembershipSimplifier I@16:54:05.167 spec-protocol> > ConstSimplifier I@16:54:05.171 spec-protocol> PASS #12: AnalysisPass I@16:54:05.243 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:54:05.243 spec-protocol> > Skolemization I@16:54:05.243 spec-protocol> > Expansion I@16:54:05.248 spec-protocol> > Remove unused let-in defs I@16:54:05.261 spec-protocol> > Running analyzers... I@16:54:05.265 spec-protocol> > Introduced expression grades I@16:54:05.267 spec-protocol> PASS #13: BoundedChecker I@16:54:05.267 spec-protocol> State 0: Checking 39 state invariants I@16:54:06.013 spec-protocol> State 0: state invariant 0 holds. I@16:54:06.014 spec-protocol> State 0: state invariant 1 holds. I@16:54:06.042 spec-protocol> State 0: state invariant 2 holds. I@16:54:06.046 spec-protocol> State 0: state invariant 3 holds. I@16:54:06.047 spec-protocol> State 0: state invariant 4 holds. I@16:54:06.071 spec-protocol> State 0: state invariant 5 holds. I@16:54:06.082 spec-protocol> State 0: state invariant 6 holds. I@16:54:06.084 spec-protocol> State 0: state invariant 7 holds. I@16:54:06.085 spec-protocol> State 0: state invariant 8 holds. I@16:54:06.086 spec-protocol> State 0: state invariant 9 holds. I@16:54:06.088 spec-protocol> State 0: state invariant 10 holds. I@16:54:06.089 spec-protocol> State 0: state invariant 11 holds. I@16:54:06.091 spec-protocol> State 0: state invariant 12 holds. I@16:54:06.099 spec-protocol> State 0: state invariant 13 holds. I@16:54:06.101 spec-protocol> State 0: state invariant 14 holds. I@16:54:06.110 spec-protocol> State 0: state invariant 15 holds. I@16:54:06.112 spec-protocol> State 0: state invariant 16 holds. I@16:54:06.113 spec-protocol> State 0: state invariant 17 holds. I@16:54:06.114 spec-protocol> State 0: state invariant 18 holds. I@16:54:06.120 spec-protocol> State 0: state invariant 19 holds. I@16:54:06.126 spec-protocol> State 0: state invariant 20 holds. I@16:54:06.134 spec-protocol> State 0: state invariant 21 holds. I@16:54:06.147 spec-protocol> State 0: state invariant 22 holds. I@16:54:06.156 spec-protocol> State 0: state invariant 23 holds. I@16:54:06.166 spec-protocol> State 0: state invariant 24 holds. I@16:54:06.167 spec-protocol> State 0: state invariant 25 holds. I@16:54:06.168 spec-protocol> State 0: state invariant 26 holds. I@16:54:06.170 spec-protocol> State 0: state invariant 27 holds. I@16:54:06.174 spec-protocol> State 0: state invariant 28 holds. I@16:54:06.199 spec-protocol> State 0: state invariant 29 holds. I@16:54:06.207 spec-protocol> State 0: state invariant 30 holds. I@16:54:06.330 spec-protocol> State 0: state invariant 31 holds. I@16:54:06.471 spec-protocol> State 0: state invariant 32 holds. I@16:54:06.624 spec-protocol> State 0: state invariant 33 holds. I@16:54:06.628 spec-protocol> State 0: state invariant 34 holds. I@16:54:06.634 spec-protocol> State 0: state invariant 35 holds. I@16:54:06.639 spec-protocol> State 0: state invariant 36 holds. I@16:54:06.640 spec-protocol> State 0: state invariant 37 holds. I@16:54:06.642 spec-protocol> State 0: state invariant 38 holds. I@16:54:06.643 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:54:06.644 spec-protocol> State 1: Checking 12 state invariants I@16:54:06.671 spec-protocol> State 1: state invariant 0 holds. I@16:54:06.673 spec-protocol> State 1: state invariant 1 holds. I@16:54:06.699 spec-protocol> State 1: state invariant 18 holds. I@16:54:06.708 spec-protocol> State 1: state invariant 19 holds. I@16:54:06.714 spec-protocol> State 1: state invariant 20 holds. I@16:54:06.722 spec-protocol> State 1: state invariant 21 holds. I@16:54:06.731 spec-protocol> State 1: state invariant 27 holds. I@16:54:06.741 spec-protocol> State 1: state invariant 28 holds. I@16:54:06.768 spec-protocol> State 1: state invariant 29 holds. I@16:54:06.775 spec-protocol> State 1: state invariant 30 holds. I@16:54:06.906 spec-protocol> State 1: state invariant 31 holds. I@16:54:07.039 spec-protocol> State 1: state invariant 32 holds. I@16:54:07.147 spec-protocol> State 1: Checking 4 state invariants I@16:54:07.171 spec-protocol> State 1: state invariant 13 holds. I@16:54:07.173 spec-protocol> State 1: state invariant 29 holds. I@16:54:07.180 spec-protocol> State 1: state invariant 30 holds. I@16:54:07.301 spec-protocol> State 1: state invariant 31 holds. I@16:54:07.430 spec-protocol> State 1: Checking 16 state invariants I@16:54:07.481 spec-protocol> State 1: state invariant 0 holds. I@16:54:07.483 spec-protocol> State 1: state invariant 1 holds. I@16:54:07.506 spec-protocol> State 1: state invariant 3 holds. I@16:54:07.510 spec-protocol> State 1: state invariant 4 holds. I@16:54:07.533 spec-protocol> State 1: state invariant 5 holds. I@16:54:07.543 spec-protocol> State 1: state invariant 18 holds. I@16:54:07.550 spec-protocol> State 1: state invariant 19 holds. I@16:54:07.557 spec-protocol> State 1: state invariant 20 holds. I@16:54:07.565 spec-protocol> State 1: state invariant 21 holds. I@16:54:07.573 spec-protocol> State 1: state invariant 23 holds. I@16:54:07.584 spec-protocol> State 1: state invariant 27 holds. I@16:54:07.589 spec-protocol> State 1: state invariant 28 holds. I@16:54:07.609 spec-protocol> State 1: state invariant 29 holds. I@16:54:07.617 spec-protocol> State 1: state invariant 30 holds. I@16:54:07.714 spec-protocol> State 1: state invariant 31 holds. I@16:54:07.828 spec-protocol> State 1: state invariant 32 holds. I@16:54:07.921 spec-protocol> State 1: Checking 6 state invariants I@16:54:07.941 spec-protocol> State 1: state invariant 2 holds. I@16:54:07.943 spec-protocol> State 1: state invariant 27 holds. I@16:54:07.960 spec-protocol> State 1: state invariant 29 holds. I@16:54:07.968 spec-protocol> State 1: state invariant 30 holds. I@16:54:08.254 spec-protocol> State 1: state invariant 31 holds. I@16:54:08.397 spec-protocol> State 1: state invariant 38 holds. I@16:54:08.400 spec-protocol> State 1: Checking 15 state invariants I@16:54:08.422 spec-protocol> State 1: state invariant 0 holds. I@16:54:08.423 spec-protocol> State 1: state invariant 1 holds. I@16:54:08.448 spec-protocol> State 1: state invariant 2 holds. I@16:54:08.450 spec-protocol> State 1: state invariant 12 holds. I@16:54:08.458 spec-protocol> State 1: state invariant 18 holds. I@16:54:08.470 spec-protocol> State 1: state invariant 19 holds. I@16:54:08.477 spec-protocol> State 1: state invariant 20 holds. I@16:54:08.489 spec-protocol> State 1: state invariant 21 holds. I@16:54:08.500 spec-protocol> State 1: state invariant 27 holds. I@16:54:08.511 spec-protocol> State 1: state invariant 28 holds. I@16:54:08.544 spec-protocol> State 1: state invariant 29 holds. I@16:54:08.554 spec-protocol> State 1: state invariant 30 holds. I@16:54:08.691 spec-protocol> State 1: state invariant 31 holds. I@16:54:08.836 spec-protocol> State 1: state invariant 32 holds. I@16:54:08.982 spec-protocol> State 1: state invariant 37 holds. I@16:54:08.986 spec-protocol> State 1: Checking 18 state invariants I@16:54:09.211 spec-protocol> State 1: state invariant 9 holds. I@16:54:09.216 spec-protocol> State 1: state invariant 10 holds. I@16:54:09.219 spec-protocol> State 1: state invariant 11 holds. I@16:54:09.220 spec-protocol> State 1: state invariant 14 holds. I@16:54:09.228 spec-protocol> State 1: state invariant 15 holds. I@16:54:09.230 spec-protocol> State 1: state invariant 17 holds. I@16:54:09.231 spec-protocol> State 1: state invariant 22 holds. I@16:54:09.239 spec-protocol> State 1: state invariant 24 holds. I@16:54:09.241 spec-protocol> State 1: state invariant 26 holds. I@16:54:09.244 spec-protocol> State 1: state invariant 27 holds. I@16:54:09.252 spec-protocol> State 1: state invariant 28 holds. I@16:54:09.275 spec-protocol> State 1: state invariant 29 holds. I@16:54:09.283 spec-protocol> State 1: state invariant 30 holds. I@16:54:09.344 spec-protocol> State 1: state invariant 31 holds. I@16:54:09.422 spec-protocol> State 1: state invariant 32 holds. I@16:54:09.544 spec-protocol> State 1: state invariant 33 holds. I@16:54:09.549 spec-protocol> State 1: state invariant 34 holds. I@16:54:09.555 spec-protocol> State 1: state invariant 35 holds. I@16:54:09.570 spec-protocol> State 1: Checking 14 state invariants I@16:54:09.800 spec-protocol> State 1: state invariant 9 holds. I@16:54:09.804 spec-protocol> State 1: state invariant 10 holds. I@16:54:09.807 spec-protocol> State 1: state invariant 11 holds. I@16:54:09.809 spec-protocol> State 1: state invariant 14 holds. I@16:54:09.817 spec-protocol> State 1: state invariant 15 holds. I@16:54:09.821 spec-protocol> State 1: state invariant 17 holds. I@16:54:09.822 spec-protocol> State 1: state invariant 24 holds. I@16:54:09.824 spec-protocol> State 1: state invariant 26 holds. I@16:54:09.827 spec-protocol> State 1: state invariant 27 holds. I@16:54:09.833 spec-protocol> State 1: state invariant 28 holds. I@16:54:09.849 spec-protocol> State 1: state invariant 29 holds. I@16:54:09.858 spec-protocol> State 1: state invariant 30 holds. I@16:54:09.915 spec-protocol> State 1: state invariant 31 holds. I@16:54:09.993 spec-protocol> State 1: state invariant 32 holds. I@16:54:10.062 spec-protocol> State 1: Checking 26 state invariants I@16:54:10.200 spec-protocol> State 1: state invariant 0 holds. I@16:54:10.202 spec-protocol> State 1: state invariant 1 holds. I@16:54:10.230 spec-protocol> State 1: state invariant 9 holds. I@16:54:10.239 spec-protocol> State 1: state invariant 10 holds. I@16:54:10.241 spec-protocol> State 1: state invariant 11 holds. I@16:54:10.244 spec-protocol> State 1: state invariant 12 holds. I@16:54:10.250 spec-protocol> State 1: state invariant 14 holds. I@16:54:10.263 spec-protocol> State 1: state invariant 15 holds. I@16:54:10.274 spec-protocol> State 1: state invariant 17 holds. I@16:54:10.277 spec-protocol> State 1: state invariant 18 holds. I@16:54:10.286 spec-protocol> State 1: state invariant 19 holds. I@16:54:10.294 spec-protocol> State 1: state invariant 20 holds. I@16:54:10.306 spec-protocol> State 1: state invariant 21 holds. I@16:54:10.322 spec-protocol> State 1: state invariant 22 holds. I@16:54:10.334 spec-protocol> State 1: state invariant 23 holds. I@16:54:10.344 spec-protocol> State 1: state invariant 24 holds. I@16:54:10.348 spec-protocol> State 1: state invariant 26 holds. I@16:54:10.352 spec-protocol> State 1: state invariant 27 holds. I@16:54:10.359 spec-protocol> State 1: state invariant 28 holds. I@16:54:10.387 spec-protocol> State 1: state invariant 29 holds. I@16:54:10.397 spec-protocol> State 1: state invariant 30 holds. I@16:54:10.586 spec-protocol> State 1: state invariant 31 holds. I@16:54:10.739 spec-protocol> State 1: state invariant 32 holds. I@16:54:10.934 spec-protocol> State 1: state invariant 33 holds. I@16:54:10.940 spec-protocol> State 1: state invariant 34 holds. I@16:54:10.949 spec-protocol> State 1: state invariant 35 holds. I@16:54:10.964 spec-protocol> State 1: Checking 22 state invariants I@16:54:11.103 spec-protocol> State 1: state invariant 0 holds. I@16:54:11.105 spec-protocol> State 1: state invariant 1 holds. I@16:54:11.137 spec-protocol> State 1: state invariant 9 holds. I@16:54:11.147 spec-protocol> State 1: state invariant 10 holds. I@16:54:11.149 spec-protocol> State 1: state invariant 11 holds. I@16:54:11.151 spec-protocol> State 1: state invariant 12 holds. I@16:54:11.158 spec-protocol> State 1: state invariant 14 holds. I@16:54:11.170 spec-protocol> State 1: state invariant 15 holds. I@16:54:11.177 spec-protocol> State 1: state invariant 17 holds. I@16:54:11.180 spec-protocol> State 1: state invariant 18 holds. I@16:54:11.188 spec-protocol> State 1: state invariant 19 holds. I@16:54:11.195 spec-protocol> State 1: state invariant 20 holds. I@16:54:11.201 spec-protocol> State 1: state invariant 21 holds. I@16:54:11.215 spec-protocol> State 1: state invariant 23 holds. I@16:54:11.225 spec-protocol> State 1: state invariant 24 holds. I@16:54:11.227 spec-protocol> State 1: state invariant 26 holds. I@16:54:11.236 spec-protocol> State 1: state invariant 27 holds. I@16:54:11.260 spec-protocol> State 1: state invariant 28 holds. I@16:54:11.299 spec-protocol> State 1: state invariant 29 holds. I@16:54:11.309 spec-protocol> State 1: state invariant 30 holds. I@16:54:11.515 spec-protocol> State 1: state invariant 31 holds. I@16:54:11.668 spec-protocol> State 1: state invariant 32 holds. I@16:54:11.817 spec-protocol> Step 1: Transition #10 is disabled I@16:54:11.861 spec-protocol> Step 1: Transition #11 is disabled I@16:54:11.901 spec-protocol> State 1: Checking 27 state invariants I@16:54:12.048 spec-protocol> State 1: state invariant 0 holds. I@16:54:12.050 spec-protocol> State 1: state invariant 1 holds. I@16:54:12.079 spec-protocol> State 1: state invariant 9 holds. I@16:54:12.095 spec-protocol> State 1: state invariant 10 holds. I@16:54:12.099 spec-protocol> State 1: state invariant 12 holds. I@16:54:12.106 spec-protocol> State 1: state invariant 13 holds. I@16:54:12.108 spec-protocol> State 1: state invariant 14 holds. I@16:54:12.117 spec-protocol> State 1: state invariant 15 holds. I@16:54:12.122 spec-protocol> State 1: state invariant 16 holds. I@16:54:12.124 spec-protocol> State 1: state invariant 17 holds. I@16:54:12.126 spec-protocol> State 1: state invariant 18 holds. I@16:54:12.134 spec-protocol> State 1: state invariant 19 holds. I@16:54:12.141 spec-protocol> State 1: state invariant 20 holds. I@16:54:12.149 spec-protocol> State 1: state invariant 21 holds. I@16:54:12.178 spec-protocol> State 1: state invariant 22 holds. I@16:54:12.194 spec-protocol> State 1: state invariant 23 holds. I@16:54:12.205 spec-protocol> State 1: state invariant 24 holds. I@16:54:12.209 spec-protocol> State 1: state invariant 26 holds. I@16:54:12.213 spec-protocol> State 1: state invariant 27 holds. I@16:54:12.234 spec-protocol> State 1: state invariant 28 holds. I@16:54:12.266 spec-protocol> State 1: state invariant 29 holds. I@16:54:12.277 spec-protocol> State 1: state invariant 30 holds. I@16:54:12.431 spec-protocol> State 1: state invariant 31 holds. I@16:54:12.570 spec-protocol> State 1: state invariant 32 holds. I@16:54:12.705 spec-protocol> State 1: state invariant 33 holds. I@16:54:12.713 spec-protocol> State 1: state invariant 34 holds. I@16:54:12.724 spec-protocol> State 1: state invariant 35 holds. I@16:54:12.739 spec-protocol> State 1: Checking 23 state invariants I@16:54:12.918 spec-protocol> State 1: state invariant 0 holds. I@16:54:12.921 spec-protocol> State 1: state invariant 1 holds. I@16:54:13.087 spec-protocol> State 1: state invariant 9 holds. I@16:54:13.098 spec-protocol> State 1: state invariant 10 holds. I@16:54:13.101 spec-protocol> State 1: state invariant 12 holds. I@16:54:13.108 spec-protocol> State 1: state invariant 13 holds. I@16:54:13.110 spec-protocol> State 1: state invariant 14 holds. I@16:54:13.118 spec-protocol> State 1: state invariant 15 holds. I@16:54:13.130 spec-protocol> State 1: state invariant 16 holds. I@16:54:13.132 spec-protocol> State 1: state invariant 17 holds. I@16:54:13.134 spec-protocol> State 1: state invariant 18 holds. I@16:54:13.154 spec-protocol> State 1: state invariant 19 holds. I@16:54:13.168 spec-protocol> State 1: state invariant 20 holds. I@16:54:13.177 spec-protocol> State 1: state invariant 21 holds. I@16:54:13.192 spec-protocol> State 1: state invariant 23 holds. I@16:54:13.202 spec-protocol> State 1: state invariant 24 holds. I@16:54:13.205 spec-protocol> State 1: state invariant 26 holds. I@16:54:13.215 spec-protocol> State 1: state invariant 27 holds. I@16:54:13.228 spec-protocol> State 1: state invariant 28 holds. I@16:54:13.261 spec-protocol> State 1: state invariant 29 holds. I@16:54:13.270 spec-protocol> State 1: state invariant 30 holds. I@16:54:13.437 spec-protocol> State 1: state invariant 31 holds. I@16:54:13.598 spec-protocol> State 1: state invariant 32 holds. I@16:54:13.743 spec-protocol> State 1: Checking 26 state invariants I@16:54:14.085 spec-protocol> State 1: state invariant 0 holds. I@16:54:14.088 spec-protocol> State 1: state invariant 1 holds. I@16:54:14.132 spec-protocol> State 1: state invariant 9 holds. I@16:54:14.151 spec-protocol> State 1: state invariant 10 holds. I@16:54:14.155 spec-protocol> State 1: state invariant 12 holds. I@16:54:14.164 spec-protocol> State 1: state invariant 14 holds. I@16:54:14.175 spec-protocol> State 1: state invariant 15 holds. I@16:54:14.182 spec-protocol> State 1: state invariant 16 holds. I@16:54:14.185 spec-protocol> State 1: state invariant 17 holds. I@16:54:14.187 spec-protocol> State 1: state invariant 18 holds. I@16:54:14.203 spec-protocol> State 1: state invariant 19 holds. I@16:54:14.219 spec-protocol> State 1: state invariant 20 holds. I@16:54:14.242 spec-protocol> State 1: state invariant 21 holds. I@16:54:14.267 spec-protocol> State 1: state invariant 22 holds. I@16:54:14.288 spec-protocol> State 1: state invariant 23 holds. I@16:54:14.302 spec-protocol> State 1: state invariant 24 holds. I@16:54:14.305 spec-protocol> State 1: state invariant 26 holds. I@16:54:14.311 spec-protocol> State 1: state invariant 27 holds. I@16:54:14.332 spec-protocol> State 1: state invariant 28 holds. I@16:54:14.384 spec-protocol> State 1: state invariant 29 holds. I@16:54:14.396 spec-protocol> State 1: state invariant 30 holds. I@16:54:14.558 spec-protocol> State 1: state invariant 31 holds. I@16:54:14.732 spec-protocol> State 1: state invariant 32 holds. I@16:54:14.957 spec-protocol> State 1: state invariant 33 holds. I@16:54:14.968 spec-protocol> State 1: state invariant 34 holds. I@16:54:14.987 spec-protocol> State 1: state invariant 35 holds. I@16:54:15.013 spec-protocol> State 1: Checking 22 state invariants I@16:54:15.344 spec-protocol> State 1: state invariant 0 holds. I@16:54:15.346 spec-protocol> State 1: state invariant 1 holds. I@16:54:15.380 spec-protocol> State 1: state invariant 9 holds. I@16:54:15.395 spec-protocol> State 1: state invariant 10 holds. I@16:54:15.399 spec-protocol> State 1: state invariant 12 holds. I@16:54:15.410 spec-protocol> State 1: state invariant 14 holds. I@16:54:15.422 spec-protocol> State 1: state invariant 15 holds. I@16:54:15.437 spec-protocol> State 1: state invariant 16 holds. I@16:54:15.441 spec-protocol> State 1: state invariant 17 holds. I@16:54:15.444 spec-protocol> State 1: state invariant 18 holds. I@16:54:15.455 spec-protocol> State 1: state invariant 19 holds. I@16:54:15.480 spec-protocol> State 1: state invariant 20 holds. I@16:54:15.496 spec-protocol> State 1: state invariant 21 holds. I@16:54:15.518 spec-protocol> State 1: state invariant 23 holds. I@16:54:15.532 spec-protocol> State 1: state invariant 24 holds. I@16:54:15.536 spec-protocol> State 1: state invariant 26 holds. I@16:54:15.548 spec-protocol> State 1: state invariant 27 holds. I@16:54:15.575 spec-protocol> State 1: state invariant 28 holds. I@16:54:15.607 spec-protocol> State 1: state invariant 29 holds. I@16:54:15.618 spec-protocol> State 1: state invariant 30 holds. I@16:54:15.791 spec-protocol> State 1: state invariant 31 holds. I@16:54:15.935 spec-protocol> State 1: state invariant 32 holds. I@16:54:16.063 spec-protocol> Step 1: Transition #16 is disabled I@16:54:16.158 spec-protocol> State 1: Checking 21 state invariants I@16:54:16.250 spec-protocol> State 1: state invariant 0 holds. I@16:54:16.252 spec-protocol> State 1: state invariant 1 holds. I@16:54:16.297 spec-protocol> State 1: state invariant 9 holds. I@16:54:16.311 spec-protocol> State 1: state invariant 10 holds. I@16:54:16.315 spec-protocol> State 1: state invariant 12 holds. I@16:54:16.326 spec-protocol> State 1: state invariant 14 holds. I@16:54:16.339 spec-protocol> State 1: state invariant 15 holds. I@16:54:16.348 spec-protocol> State 1: state invariant 17 holds. I@16:54:16.352 spec-protocol> State 1: state invariant 18 holds. I@16:54:16.368 spec-protocol> State 1: state invariant 19 holds. I@16:54:16.388 spec-protocol> State 1: state invariant 20 holds. I@16:54:16.410 spec-protocol> State 1: state invariant 21 holds. I@16:54:16.440 spec-protocol> State 1: state invariant 23 holds. I@16:54:16.454 spec-protocol> State 1: state invariant 24 holds. I@16:54:16.459 spec-protocol> State 1: state invariant 26 holds. I@16:54:16.463 spec-protocol> State 1: state invariant 27 holds. I@16:54:16.478 spec-protocol> State 1: state invariant 28 holds. I@16:54:16.515 spec-protocol> State 1: state invariant 29 holds. I@16:54:16.527 spec-protocol> State 1: state invariant 30 holds. I@16:54:16.744 spec-protocol> State 1: state invariant 31 holds. I@16:54:16.982 spec-protocol> State 1: state invariant 32 holds. I@16:54:17.155 spec-protocol> Step 1: Transition #18 is disabled I@16:54:17.209 spec-protocol> State 1: Checking 21 state invariants I@16:54:17.284 spec-protocol> State 1: state invariant 0 holds. I@16:54:17.285 spec-protocol> State 1: state invariant 1 holds. I@16:54:17.321 spec-protocol> State 1: state invariant 9 holds. I@16:54:17.334 spec-protocol> State 1: state invariant 10 holds. I@16:54:17.337 spec-protocol> State 1: state invariant 12 holds. I@16:54:17.346 spec-protocol> State 1: state invariant 14 holds. I@16:54:17.358 spec-protocol> State 1: state invariant 15 holds. I@16:54:17.364 spec-protocol> State 1: state invariant 17 holds. I@16:54:17.366 spec-protocol> State 1: state invariant 18 holds. I@16:54:17.377 spec-protocol> State 1: state invariant 19 holds. I@16:54:17.393 spec-protocol> State 1: state invariant 20 holds. I@16:54:17.405 spec-protocol> State 1: state invariant 21 holds. I@16:54:17.427 spec-protocol> State 1: state invariant 23 holds. I@16:54:17.440 spec-protocol> State 1: state invariant 24 holds. I@16:54:17.444 spec-protocol> State 1: state invariant 26 holds. I@16:54:17.449 spec-protocol> State 1: state invariant 27 holds. I@16:54:17.477 spec-protocol> State 1: state invariant 28 holds. I@16:54:17.536 spec-protocol> State 1: state invariant 29 holds. I@16:54:17.547 spec-protocol> State 1: state invariant 30 holds. I@16:54:17.803 spec-protocol> State 1: state invariant 31 holds. I@16:54:18.090 spec-protocol> State 1: state invariant 32 holds. I@16:54:18.297 spec-protocol> Step 1: Transition #20 is disabled I@16:54:18.351 spec-protocol> Step 1: Transition #21 is disabled I@16:54:18.418 spec-protocol> State 1: Checking 14 state invariants I@16:54:18.525 spec-protocol> State 1: state invariant 6 holds. I@16:54:18.527 spec-protocol> State 1: state invariant 7 holds. I@16:54:18.531 spec-protocol> State 1: state invariant 22 holds. I@16:54:18.552 spec-protocol> State 1: state invariant 25 holds. I@16:54:18.563 spec-protocol> State 1: state invariant 27 holds. I@16:54:18.603 spec-protocol> State 1: state invariant 28 holds. I@16:54:18.644 spec-protocol> State 1: state invariant 29 holds. I@16:54:18.654 spec-protocol> State 1: state invariant 30 holds. I@16:54:18.843 spec-protocol> State 1: state invariant 31 holds. I@16:54:18.950 spec-protocol> State 1: state invariant 32 holds. I@16:54:19.079 spec-protocol> State 1: state invariant 33 holds. I@16:54:19.086 spec-protocol> State 1: state invariant 34 holds. I@16:54:19.094 spec-protocol> State 1: state invariant 35 holds. I@16:54:19.101 spec-protocol> State 1: state invariant 38 holds. I@16:54:19.104 spec-protocol> State 1: Checking 17 state invariants I@16:54:19.187 spec-protocol> State 1: state invariant 3 holds. I@16:54:19.191 spec-protocol> State 1: state invariant 4 holds. I@16:54:19.243 spec-protocol> State 1: state invariant 5 holds. I@16:54:19.284 spec-protocol> State 1: state invariant 6 holds. I@16:54:19.287 spec-protocol> State 1: state invariant 7 holds. I@16:54:19.289 spec-protocol> State 1: state invariant 22 holds. I@16:54:19.305 spec-protocol> State 1: state invariant 25 holds. I@16:54:19.308 spec-protocol> State 1: state invariant 27 holds. I@16:54:19.314 spec-protocol> State 1: state invariant 28 holds. I@16:54:19.348 spec-protocol> State 1: state invariant 29 holds. I@16:54:19.357 spec-protocol> State 1: state invariant 30 holds. I@16:54:19.610 spec-protocol> State 1: state invariant 31 holds. I@16:54:19.780 spec-protocol> State 1: state invariant 32 holds. I@16:54:20.009 spec-protocol> State 1: state invariant 33 holds. I@16:54:20.020 spec-protocol> State 1: state invariant 34 holds. I@16:54:20.029 spec-protocol> State 1: state invariant 35 holds. I@16:54:20.037 spec-protocol> State 1: state invariant 38 holds. I@16:54:20.040 spec-protocol> Step 1: picking a transition out of 17 transition(s) I@16:54:20.042 spec-protocol> The outcome is: NoError I@16:54:20.491 spec-protocol> > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... spec-protocol> PASS #0: SanyParser I@16:54:20.719 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:54:20.849 spec-protocol> > Running Snowcat .::. I@16:54:20.850 spec-protocol> > Your types are purrfect! I@16:54:22.818 spec-protocol> > All expressions are typed I@16:54:22.818 spec-protocol> PASS #2: ConfigurationPass I@16:54:22.819 spec-protocol> > Set the initialization predicate to q::inductiveInv I@16:54:22.819 spec-protocol> > Set the transition predicate to q::step I@16:54:22.819 spec-protocol> > Set an invariant to q::inv I@16:54:22.820 spec-protocol> PASS #3: DesugarerPass I@16:54:22.821 spec-protocol> > Desugaring... I@16:54:22.821 spec-protocol> PASS #4: InlinePass I@16:54:22.823 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:54:22.823 spec-protocol> PASS #5: TemporalPass I@16:54:22.849 spec-protocol> > Rewriting temporal operators... I@16:54:22.849 spec-protocol> > No temporal property specified, nothing to encode I@16:54:22.849 spec-protocol> PASS #6: InlinePass I@16:54:22.849 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:54:22.849 spec-protocol> PASS #7: PrimingPass I@16:54:22.860 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:22.860 spec-protocol> PASS #8: VCGen I@16:54:22.861 spec-protocol> > Producing verification conditions from the invariant q::inv I@16:54:22.861 spec-protocol> > VCGen produced 5 verification condition(s) I@16:54:22.861 spec-protocol> PASS #9: PreprocessingPass I@16:54:22.862 spec-protocol> > Before preprocessing: unique renaming I@16:54:22.862 spec-protocol> > Applying standard transformations: I@16:54:22.862 spec-protocol> > PrimePropagation I@16:54:22.862 spec-protocol> > Desugarer I@16:54:22.866 spec-protocol> > UniqueRenamer I@16:54:22.870 spec-protocol> > Normalizer I@16:54:22.879 spec-protocol> > SetMembershipSimplifier I@16:54:22.884 spec-protocol> > Keramelizer I@16:54:22.887 spec-protocol> > After preprocessing: UniqueRenamer I@16:54:22.895 spec-protocol> PASS #10: TransitionFinderPass I@16:54:22.907 spec-protocol> > Found 1 initializing transitions I@16:54:22.909 spec-protocol> > Found 24 transitions I@16:54:22.918 spec-protocol> > No constant initializer I@16:54:22.919 spec-protocol> > Applying unique renaming I@16:54:22.919 spec-protocol> PASS #11: OptimizationPass I@16:54:22.935 spec-protocol> > Applying optimizations: I@16:54:22.935 spec-protocol> > ConstSimplifier I@16:54:22.935 spec-protocol> > ExprOptimizer I@16:54:22.995 spec-protocol> > SetMembershipSimplifier I@16:54:23.002 spec-protocol> > ConstSimplifier I@16:54:23.006 spec-protocol> PASS #12: AnalysisPass I@16:54:23.063 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:54:23.063 spec-protocol> > Skolemization I@16:54:23.063 spec-protocol> > Expansion I@16:54:23.066 spec-protocol> > Remove unused let-in defs I@16:54:23.078 spec-protocol> > Running analyzers... I@16:54:23.081 spec-protocol> > Introduced expression grades I@16:54:23.082 spec-protocol> PASS #13: BoundedChecker I@16:54:23.083 spec-protocol> State 0: Checking 5 state invariants I@16:54:23.624 spec-protocol> State 0: state invariant 0 holds. I@16:54:23.625 spec-protocol> State 0: state invariant 1 holds. I@16:54:23.626 spec-protocol> State 0: state invariant 2 holds. I@16:54:23.628 spec-protocol> State 0: state invariant 3 holds. I@16:54:23.632 spec-protocol> State 0: state invariant 4 holds. I@16:54:23.663 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:54:23.666 spec-protocol> The outcome is: NoError I@16:54:23.680 spec-protocol> [ok] No violation found (31962ms). 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