this derivation will be built: /nix/store/dya24l1lmm138d3b1826q2h2fhp5vrh2-spec-protocol.drv building '/nix/store/dya24l1lmm138d3b1826q2h2fhp5vrh2-spec-protocol.drv' 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-09-01T10-46-37_9135534759269904332 spec-protocol> # APALACHE version: 0.56.1 | build: 70cdaf4 I@10:46:37.861 spec-protocol> Starting checker server on port 8822... I@10:46:37.902 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: a2:96:78:c0:1e:20:c2:8f W@10:46:42.515 spec-protocol> Sep 01, 2026 10:46:46 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@10:46:50.289 spec-protocol> PASS #1: TypeCheckerSnowcat I@10:46:56.404 spec-protocol> > Running Snowcat .::. I@10:46:56.404 spec-protocol> > Your types are purrfect! I@10:47:09.401 spec-protocol> > All expressions are typed I@10:47:09.437 spec-protocol> PASS #2: ConfigurationPass I@10:47:09.439 spec-protocol> > Set the initialization predicate to q::init I@10:47:09.487 spec-protocol> > Set the transition predicate to q::step I@10:47:09.488 spec-protocol> > Set an invariant to q::inductiveInv I@10:47:09.496 spec-protocol> PASS #3: DesugarerPass I@10:47:09.565 spec-protocol> > Desugaring... I@10:47:09.565 spec-protocol> PASS #4: InlinePass I@10:47:09.949 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@10:47:09.956 spec-protocol> PASS #5: TemporalPass I@10:47:10.816 spec-protocol> > Rewriting temporal operators... I@10:47:10.816 spec-protocol> > No temporal property specified, nothing to encode I@10:47:10.816 spec-protocol> PASS #6: InlinePass I@10:47:10.823 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@10:47:10.824 spec-protocol> PASS #7: PrimingPass I@10:47:11.047 spec-protocol> > Introducing q::initPrimed for q::init' I@10:47:11.062 spec-protocol> PASS #8: VCGen I@10:47:11.080 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@10:47:11.084 spec-protocol> > VCGen produced 39 verification condition(s) I@10:47:11.168 spec-protocol> PASS #9: PreprocessingPass I@10:47:11.273 spec-protocol> > Before preprocessing: unique renaming I@10:47:11.273 spec-protocol> > Applying standard transformations: I@10:47:11.287 spec-protocol> > PrimePropagation I@10:47:11.288 spec-protocol> > Desugarer I@10:47:11.320 spec-protocol> > UniqueRenamer I@10:47:11.355 spec-protocol> > Normalizer I@10:47:11.561 spec-protocol> > Keramelizer I@10:47:11.768 spec-protocol> > After preprocessing: UniqueRenamer I@10:47:11.916 spec-protocol> PASS #10: TransitionFinderPass I@10:47:12.397 spec-protocol> > Found 1 initializing transitions I@10:47:12.456 spec-protocol> > Found 24 transitions I@10:47:13.006 spec-protocol> > No constant initializer I@10:47:13.011 spec-protocol> > Applying unique renaming I@10:47:13.036 spec-protocol> PASS #11: OptimizationPass I@10:47:13.499 spec-protocol> > Applying optimizations: I@10:47:13.552 spec-protocol> > ConstSimplifier I@10:47:13.553 spec-protocol> > ExprOptimizer I@10:47:14.316 spec-protocol> > SetMembershipSimplifier I@10:47:14.637 spec-protocol> > ConstSimplifier I@10:47:14.762 spec-protocol> PASS #12: AnalysisPass I@10:47:15.225 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@10:47:15.228 spec-protocol> > Skolemization I@10:47:15.229 spec-protocol> > Expansion I@10:47:15.238 spec-protocol> > Remove unused let-in defs I@10:47:15.275 spec-protocol> > Running analyzers... I@10:47:15.408 spec-protocol> > Introduced expression grades I@10:47:15.495 spec-protocol> PASS #13: BoundedChecker I@10:47:15.495 spec-protocol> State 0: Checking 39 state invariants I@10:47:16.487 spec-protocol> State 0: state invariant 0 holds. I@10:47:16.494 spec-protocol> State 0: state invariant 1 holds. I@10:47:16.997 spec-protocol> State 0: state invariant 2 holds. I@10:47:17.003 spec-protocol> State 0: state invariant 3 holds. I@10:47:17.004 spec-protocol> State 0: state invariant 4 holds. I@10:47:17.154 spec-protocol> State 0: state invariant 5 holds. I@10:47:17.164 spec-protocol> State 0: state invariant 6 holds. I@10:47:17.167 spec-protocol> State 0: state invariant 7 holds. I@10:47:17.173 spec-protocol> State 0: state invariant 8 holds. I@10:47:17.180 spec-protocol> State 0: state invariant 9 holds. I@10:47:17.226 spec-protocol> State 0: state invariant 10 holds. I@10:47:17.227 spec-protocol> State 0: state invariant 11 holds. I@10:47:17.228 spec-protocol> State 0: state invariant 12 holds. I@10:47:17.257 spec-protocol> State 0: state invariant 13 holds. I@10:47:17.262 spec-protocol> State 0: state invariant 14 holds. I@10:47:17.289 spec-protocol> State 0: state invariant 15 holds. I@10:47:17.291 spec-protocol> State 0: state invariant 16 holds. I@10:47:17.292 spec-protocol> State 0: state invariant 17 holds. I@10:47:17.292 spec-protocol> State 0: state invariant 18 holds. I@10:47:17.297 spec-protocol> State 0: state invariant 19 holds. I@10:47:17.304 spec-protocol> State 0: state invariant 20 holds. I@10:47:17.315 spec-protocol> State 0: state invariant 21 holds. I@10:47:17.326 spec-protocol> State 0: state invariant 22 holds. I@10:47:17.344 spec-protocol> State 0: state invariant 23 holds. I@10:47:17.379 spec-protocol> State 0: state invariant 24 holds. I@10:47:17.393 spec-protocol> State 0: state invariant 25 holds. I@10:47:17.397 spec-protocol> State 0: state invariant 26 holds. I@10:47:17.435 spec-protocol> State 0: state invariant 27 holds. I@10:47:17.478 spec-protocol> State 0: state invariant 28 holds. I@10:47:17.550 spec-protocol> State 0: state invariant 29 holds. I@10:47:17.579 spec-protocol> State 0: state invariant 30 holds. I@10:47:17.670 spec-protocol> State 0: state invariant 31 holds. I@10:47:17.821 spec-protocol> State 0: state invariant 32 holds. I@10:47:17.929 spec-protocol> State 0: state invariant 33 holds. I@10:47:17.931 spec-protocol> State 0: state invariant 34 holds. I@10:47:17.939 spec-protocol> State 0: state invariant 35 holds. I@10:47:17.946 spec-protocol> State 0: state invariant 36 holds. I@10:47:17.949 spec-protocol> State 0: state invariant 37 holds. I@10:47:17.951 spec-protocol> State 0: state invariant 38 holds. I@10:47:17.952 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@10:47:17.953 spec-protocol> The outcome is: NoError I@10:47:17.964 spec-protocol> > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... spec-protocol> PASS #0: SanyParser I@10:47:20.424 spec-protocol> PASS #1: TypeCheckerSnowcat I@10:47:21.926 spec-protocol> > Running Snowcat .::. I@10:47:21.926 spec-protocol> > Your types are purrfect! I@10:47:35.072 spec-protocol> > All expressions are typed I@10:47:35.073 spec-protocol> PASS #2: ConfigurationPass I@10:47:35.074 spec-protocol> > Set the initialization predicate to q::inductiveInv I@10:47:35.075 spec-protocol> > Set the transition predicate to q::step I@10:47:35.075 spec-protocol> > Set an invariant to q::inductiveInv I@10:47:35.076 spec-protocol> PASS #3: DesugarerPass I@10:47:35.083 spec-protocol> > Desugaring... I@10:47:35.083 spec-protocol> PASS #4: InlinePass I@10:47:35.091 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@10:47:35.091 spec-protocol> PASS #5: TemporalPass I@10:47:35.404 spec-protocol> > Rewriting temporal operators... I@10:47:35.407 spec-protocol> > No temporal property specified, nothing to encode I@10:47:35.408 spec-protocol> PASS #6: InlinePass I@10:47:35.408 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@10:47:35.408 spec-protocol> PASS #7: PrimingPass I@10:47:35.462 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@10:47:35.462 spec-protocol> PASS #8: VCGen I@10:47:35.465 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@10:47:35.465 spec-protocol> > VCGen produced 39 verification condition(s) I@10:47:35.467 spec-protocol> PASS #9: PreprocessingPass I@10:47:35.476 spec-protocol> > Before preprocessing: unique renaming I@10:47:35.480 spec-protocol> > Applying standard transformations: I@10:47:35.482 spec-protocol> > PrimePropagation I@10:47:35.484 spec-protocol> > Desugarer I@10:47:35.492 spec-protocol> > UniqueRenamer I@10:47:35.513 spec-protocol> > Normalizer I@10:47:35.547 spec-protocol> > Keramelizer I@10:47:35.565 spec-protocol> > After preprocessing: UniqueRenamer I@10:47:35.629 spec-protocol> PASS #10: TransitionFinderPass I@10:47:35.697 spec-protocol> > Found 1 initializing transitions I@10:47:35.704 spec-protocol> > Found 24 transitions I@10:47:35.748 spec-protocol> > No constant initializer I@10:47:35.749 spec-protocol> > Applying unique renaming I@10:47:35.749 spec-protocol> PASS #11: OptimizationPass I@10:47:35.869 spec-protocol> > Applying optimizations: I@10:47:35.869 spec-protocol> > ConstSimplifier I@10:47:35.869 spec-protocol> > ExprOptimizer I@10:47:36.270 spec-protocol> > SetMembershipSimplifier I@10:47:36.293 spec-protocol> > ConstSimplifier I@10:47:36.304 spec-protocol> PASS #12: AnalysisPass I@10:47:36.426 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@10:47:36.427 spec-protocol> > Skolemization I@10:47:36.427 spec-protocol> > Expansion I@10:47:36.435 spec-protocol> > Remove unused let-in defs I@10:47:36.723 spec-protocol> > Running analyzers... I@10:47:36.769 spec-protocol> > Introduced expression grades I@10:47:36.781 spec-protocol> PASS #13: BoundedChecker I@10:47:36.784 spec-protocol> State 0: Checking 39 state invariants I@10:47:39.693 spec-protocol> State 0: state invariant 0 holds. I@10:47:39.695 spec-protocol> State 0: state invariant 1 holds. I@10:47:39.746 spec-protocol> State 0: state invariant 2 holds. I@10:47:39.752 spec-protocol> State 0: state invariant 3 holds. I@10:47:39.756 spec-protocol> State 0: state invariant 4 holds. I@10:47:39.799 spec-protocol> State 0: state invariant 5 holds. I@10:47:39.829 spec-protocol> State 0: state invariant 6 holds. I@10:47:39.832 spec-protocol> State 0: state invariant 7 holds. I@10:47:39.836 spec-protocol> State 0: state invariant 8 holds. I@10:47:39.844 spec-protocol> State 0: state invariant 9 holds. I@10:47:39.848 spec-protocol> State 0: state invariant 10 holds. I@10:47:39.853 spec-protocol> State 0: state invariant 11 holds. I@10:47:39.857 spec-protocol> State 0: state invariant 12 holds. I@10:47:39.882 spec-protocol> State 0: state invariant 13 holds. I@10:47:39.889 spec-protocol> State 0: state invariant 14 holds. I@10:47:39.926 spec-protocol> State 0: state invariant 15 holds. I@10:47:39.933 spec-protocol> State 0: state invariant 16 holds. I@10:47:39.941 spec-protocol> State 0: state invariant 17 holds. I@10:47:39.952 spec-protocol> State 0: state invariant 18 holds. I@10:47:39.995 spec-protocol> State 0: state invariant 19 holds. I@10:47:40.010 spec-protocol> State 0: state invariant 20 holds. I@10:47:40.030 spec-protocol> State 0: state invariant 21 holds. I@10:47:40.065 spec-protocol> State 0: state invariant 22 holds. I@10:47:40.085 spec-protocol> State 0: state invariant 23 holds. I@10:47:40.101 spec-protocol> State 0: state invariant 24 holds. I@10:47:40.104 spec-protocol> State 0: state invariant 25 holds. I@10:47:40.106 spec-protocol> State 0: state invariant 26 holds. I@10:47:40.110 spec-protocol> State 0: state invariant 27 holds. I@10:47:40.121 spec-protocol> State 0: state invariant 28 holds. I@10:47:40.200 spec-protocol> State 0: state invariant 29 holds. I@10:47:40.215 spec-protocol> State 0: state invariant 30 holds. I@10:47:40.541 spec-protocol> State 0: state invariant 31 holds. I@10:47:40.967 spec-protocol> State 0: state invariant 32 holds. I@10:47:41.494 spec-protocol> State 0: state invariant 33 holds. I@10:47:41.507 spec-protocol> State 0: state invariant 34 holds. I@10:47:41.533 spec-protocol> State 0: state invariant 35 holds. I@10:47:41.564 spec-protocol> State 0: state invariant 36 holds. I@10:47:41.573 spec-protocol> State 0: state invariant 37 holds. I@10:47:41.583 spec-protocol> State 0: state invariant 38 holds. I@10:47:41.598 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@10:47:41.611 spec-protocol> State 1: Checking 12 state invariants I@10:47:41.720 spec-protocol> State 1: state invariant 0 holds. I@10:47:41.723 spec-protocol> State 1: state invariant 1 holds. I@10:47:41.772 spec-protocol> State 1: state invariant 18 holds. I@10:47:41.793 spec-protocol> State 1: state invariant 19 holds. I@10:47:41.807 spec-protocol> State 1: state invariant 20 holds. I@10:47:41.829 spec-protocol> State 1: state invariant 21 holds. I@10:47:41.855 spec-protocol> State 1: state invariant 27 holds. I@10:47:41.877 spec-protocol> State 1: state invariant 28 holds. I@10:47:41.935 spec-protocol> State 1: state invariant 29 holds. I@10:47:41.948 spec-protocol> State 1: state invariant 30 holds. I@10:47:42.889 spec-protocol> State 1: state invariant 31 holds. I@10:47:43.630 spec-protocol> State 1: state invariant 32 holds. I@10:47:44.403 spec-protocol> State 1: Checking 4 state invariants I@10:47:44.562 spec-protocol> State 1: state invariant 13 holds. I@10:47:44.572 spec-protocol> State 1: state invariant 29 holds. I@10:47:44.613 spec-protocol> State 1: state invariant 30 holds. I@10:47:45.563 spec-protocol> State 1: state invariant 31 holds. I@10:47:46.079 spec-protocol> State 1: Checking 16 state invariants I@10:47:46.394 spec-protocol> State 1: state invariant 0 holds. I@10:47:46.397 spec-protocol> State 1: state invariant 1 holds. I@10:47:46.437 spec-protocol> State 1: state invariant 3 holds. I@10:47:46.443 spec-protocol> State 1: state invariant 4 holds. I@10:47:46.481 spec-protocol> State 1: state invariant 5 holds. I@10:47:46.510 spec-protocol> State 1: state invariant 18 holds. I@10:47:46.532 spec-protocol> State 1: state invariant 19 holds. I@10:47:46.558 spec-protocol> State 1: state invariant 20 holds. I@10:47:46.577 spec-protocol> State 1: state invariant 21 holds. I@10:47:46.621 spec-protocol> State 1: state invariant 23 holds. I@10:47:46.639 spec-protocol> State 1: state invariant 27 holds. I@10:47:46.647 spec-protocol> State 1: state invariant 28 holds. I@10:47:46.682 spec-protocol> State 1: state invariant 29 holds. I@10:47:46.693 spec-protocol> State 1: state invariant 30 holds. I@10:47:47.117 spec-protocol> State 1: state invariant 31 holds. I@10:47:47.502 spec-protocol> State 1: state invariant 32 holds. I@10:47:48.192 spec-protocol> State 1: Checking 6 state invariants I@10:47:48.252 spec-protocol> State 1: state invariant 2 holds. I@10:47:48.256 spec-protocol> State 1: state invariant 27 holds. I@10:47:48.280 spec-protocol> State 1: state invariant 29 holds. I@10:47:48.303 spec-protocol> State 1: state invariant 30 holds. I@10:47:48.927 spec-protocol> State 1: state invariant 31 holds. I@10:47:50.087 spec-protocol> State 1: state invariant 38 holds. I@10:47:50.106 spec-protocol> State 1: Checking 15 state invariants I@10:47:50.343 spec-protocol> State 1: state invariant 0 holds. I@10:47:50.363 spec-protocol> State 1: state invariant 1 holds. I@10:47:50.628 spec-protocol> State 1: state invariant 2 holds. I@10:47:50.638 spec-protocol> State 1: state invariant 12 holds. I@10:47:50.743 spec-protocol> State 1: state invariant 18 holds. I@10:47:50.834 spec-protocol> State 1: state invariant 19 holds. I@10:47:50.908 spec-protocol> State 1: state invariant 20 holds. I@10:47:50.997 spec-protocol> State 1: state invariant 21 holds. I@10:47:51.024 spec-protocol> State 1: state invariant 27 holds. I@10:47:51.056 spec-protocol> State 1: state invariant 28 holds. I@10:47:51.149 spec-protocol> State 1: state invariant 29 holds. I@10:47:51.167 spec-protocol> State 1: state invariant 30 holds. I@10:47:52.288 spec-protocol> State 1: state invariant 31 holds. I@10:47:53.149 spec-protocol> State 1: state invariant 32 holds. I@10:47:53.825 spec-protocol> State 1: state invariant 37 holds. I@10:47:53.832 spec-protocol> State 1: Checking 18 state invariants I@10:47:54.382 spec-protocol> State 1: state invariant 9 holds. I@10:47:54.392 spec-protocol> State 1: state invariant 10 holds. I@10:47:54.396 spec-protocol> State 1: state invariant 11 holds. I@10:47:54.399 spec-protocol> State 1: state invariant 14 holds. I@10:47:54.413 spec-protocol> State 1: state invariant 15 holds. I@10:47:54.418 spec-protocol> State 1: state invariant 17 holds. I@10:47:54.422 spec-protocol> State 1: state invariant 22 holds. I@10:47:54.440 spec-protocol> State 1: state invariant 24 holds. I@10:47:54.444 spec-protocol> State 1: state invariant 26 holds. I@10:47:54.451 spec-protocol> State 1: state invariant 27 holds. I@10:47:54.468 spec-protocol> State 1: state invariant 28 holds. I@10:47:54.511 spec-protocol> State 1: state invariant 29 holds. I@10:47:54.539 spec-protocol> State 1: state invariant 30 holds. I@10:47:54.682 spec-protocol> State 1: state invariant 31 holds. I@10:47:54.893 spec-protocol> State 1: state invariant 32 holds. I@10:47:55.243 spec-protocol> State 1: state invariant 33 holds. I@10:47:55.259 spec-protocol> State 1: state invariant 34 holds. I@10:47:55.273 spec-protocol> State 1: state invariant 35 holds. I@10:47:55.316 spec-protocol> State 1: Checking 14 state invariants I@10:47:56.726 spec-protocol> State 1: state invariant 9 holds. I@10:47:56.737 spec-protocol> State 1: state invariant 10 holds. I@10:47:56.744 spec-protocol> State 1: state invariant 11 holds. I@10:47:56.755 spec-protocol> State 1: state invariant 14 holds. I@10:47:56.790 spec-protocol> State 1: state invariant 15 holds. I@10:47:56.809 spec-protocol> State 1: state invariant 17 holds. I@10:47:56.820 spec-protocol> State 1: state invariant 24 holds. I@10:47:56.832 spec-protocol> State 1: state invariant 26 holds. I@10:47:56.846 spec-protocol> State 1: state invariant 27 holds. I@10:47:56.868 spec-protocol> State 1: state invariant 28 holds. I@10:47:56.896 spec-protocol> State 1: state invariant 29 holds. I@10:47:56.909 spec-protocol> State 1: state invariant 30 holds. I@10:47:57.121 spec-protocol> State 1: state invariant 31 holds. I@10:47:57.247 spec-protocol> State 1: state invariant 32 holds. I@10:47:57.495 spec-protocol> State 1: Checking 26 state invariants I@10:47:58.513 spec-protocol> State 1: state invariant 0 holds. I@10:47:58.518 spec-protocol> State 1: state invariant 1 holds. I@10:47:58.596 spec-protocol> State 1: state invariant 9 holds. I@10:47:58.620 spec-protocol> State 1: state invariant 10 holds. I@10:47:58.625 spec-protocol> State 1: state invariant 11 holds. I@10:47:58.630 spec-protocol> State 1: state invariant 12 holds. I@10:47:58.683 spec-protocol> State 1: state invariant 14 holds. I@10:47:58.741 spec-protocol> State 1: state invariant 15 holds. I@10:47:58.774 spec-protocol> State 1: state invariant 17 holds. I@10:47:58.780 spec-protocol> State 1: state invariant 18 holds. I@10:47:58.808 spec-protocol> State 1: state invariant 19 holds. I@10:47:58.866 spec-protocol> State 1: state invariant 20 holds. I@10:47:58.907 spec-protocol> State 1: state invariant 21 holds. I@10:47:59.060 spec-protocol> State 1: state invariant 22 holds. I@10:47:59.210 spec-protocol> State 1: state invariant 23 holds. I@10:47:59.261 spec-protocol> State 1: state invariant 24 holds. I@10:47:59.293 spec-protocol> State 1: state invariant 26 holds. I@10:47:59.357 spec-protocol> State 1: state invariant 27 holds. I@10:47:59.862 spec-protocol> State 1: state invariant 28 holds. I@10:48:00.067 spec-protocol> State 1: state invariant 29 holds. I@10:48:00.107 spec-protocol> State 1: state invariant 30 holds. I@10:48:01.322 spec-protocol> State 1: state invariant 31 holds. I@10:48:04.677 spec-protocol> State 1: state invariant 32 holds. I@10:48:06.215 spec-protocol> State 1: state invariant 33 holds. I@10:48:06.232 spec-protocol> State 1: state invariant 34 holds. I@10:48:06.275 spec-protocol> State 1: state invariant 35 holds. I@10:48:06.419 spec-protocol> State 1: Checking 22 state invariants I@10:48:07.283 spec-protocol> State 1: state invariant 0 holds. I@10:48:07.303 spec-protocol> State 1: state invariant 1 holds. I@10:48:07.676 spec-protocol> State 1: state invariant 9 holds. I@10:48:07.797 spec-protocol> State 1: state invariant 10 holds. I@10:48:07.831 spec-protocol> State 1: state invariant 11 holds. I@10:48:07.858 spec-protocol> State 1: state invariant 12 holds. I@10:48:07.938 spec-protocol> State 1: state invariant 14 holds. I@10:48:08.010 spec-protocol> State 1: state invariant 15 holds. I@10:48:08.054 spec-protocol> State 1: state invariant 17 holds. I@10:48:08.069 spec-protocol> State 1: state invariant 18 holds. I@10:48:08.110 spec-protocol> State 1: state invariant 19 holds. I@10:48:08.126 spec-protocol> State 1: state invariant 20 holds. I@10:48:08.164 spec-protocol> State 1: state invariant 21 holds. I@10:48:08.263 spec-protocol> State 1: state invariant 23 holds. I@10:48:08.285 spec-protocol> State 1: state invariant 24 holds. I@10:48:08.290 spec-protocol> State 1: state invariant 26 holds. I@10:48:08.315 spec-protocol> State 1: state invariant 27 holds. I@10:48:08.430 spec-protocol> State 1: state invariant 28 holds. I@10:48:08.750 spec-protocol> State 1: state invariant 29 holds. I@10:48:08.796 spec-protocol> State 1: state invariant 30 holds. I@10:48:10.142 spec-protocol> State 1: state invariant 31 holds. I@10:48:11.127 spec-protocol> State 1: state invariant 32 holds. I@10:48:12.165 spec-protocol> Step 1: Transition #10 is disabled I@10:48:12.285 spec-protocol> Step 1: Transition #11 is disabled I@10:48:12.348 spec-protocol> State 1: Checking 27 state invariants I@10:48:12.967 spec-protocol> State 1: state invariant 0 holds. I@10:48:12.972 spec-protocol> State 1: state invariant 1 holds. I@10:48:13.035 spec-protocol> State 1: state invariant 9 holds. I@10:48:13.064 spec-protocol> State 1: state invariant 10 holds. I@10:48:13.069 spec-protocol> State 1: state invariant 12 holds. I@10:48:13.082 spec-protocol> State 1: state invariant 13 holds. I@10:48:13.087 spec-protocol> State 1: state invariant 14 holds. I@10:48:13.103 spec-protocol> State 1: state invariant 15 holds. I@10:48:13.134 spec-protocol> State 1: state invariant 16 holds. I@10:48:13.139 spec-protocol> State 1: state invariant 17 holds. I@10:48:13.144 spec-protocol> State 1: state invariant 18 holds. I@10:48:13.175 spec-protocol> State 1: state invariant 19 holds. I@10:48:13.205 spec-protocol> State 1: state invariant 20 holds. I@10:48:13.242 spec-protocol> State 1: state invariant 21 holds. I@10:48:13.277 spec-protocol> State 1: state invariant 22 holds. I@10:48:13.318 spec-protocol> State 1: state invariant 23 holds. I@10:48:13.334 spec-protocol> State 1: state invariant 24 holds. I@10:48:13.339 spec-protocol> State 1: state invariant 26 holds. I@10:48:13.348 spec-protocol> State 1: state invariant 27 holds. I@10:48:13.419 spec-protocol> State 1: state invariant 28 holds. I@10:48:13.587 spec-protocol> State 1: state invariant 29 holds. I@10:48:13.661 spec-protocol> State 1: state invariant 30 holds. I@10:48:14.417 spec-protocol> State 1: state invariant 31 holds. I@10:48:14.796 spec-protocol> State 1: state invariant 32 holds. I@10:48:15.180 spec-protocol> State 1: state invariant 33 holds. I@10:48:15.188 spec-protocol> State 1: state invariant 34 holds. I@10:48:15.202 spec-protocol> State 1: state invariant 35 holds. I@10:48:15.236 spec-protocol> State 1: Checking 23 state invariants I@10:48:15.582 spec-protocol> State 1: state invariant 0 holds. I@10:48:15.595 spec-protocol> State 1: state invariant 1 holds. I@10:48:15.654 spec-protocol> State 1: state invariant 9 holds. I@10:48:15.675 spec-protocol> State 1: state invariant 10 holds. I@10:48:15.681 spec-protocol> State 1: state invariant 12 holds. I@10:48:15.692 spec-protocol> State 1: state invariant 13 holds. I@10:48:15.698 spec-protocol> State 1: state invariant 14 holds. I@10:48:15.713 spec-protocol> State 1: state invariant 15 holds. I@10:48:15.767 spec-protocol> State 1: state invariant 16 holds. I@10:48:15.772 spec-protocol> State 1: state invariant 17 holds. I@10:48:15.783 spec-protocol> State 1: state invariant 18 holds. I@10:48:15.837 spec-protocol> State 1: state invariant 19 holds. I@10:48:15.868 spec-protocol> State 1: state invariant 20 holds. I@10:48:15.890 spec-protocol> State 1: state invariant 21 holds. I@10:48:15.928 spec-protocol> State 1: state invariant 23 holds. I@10:48:15.943 spec-protocol> State 1: state invariant 24 holds. I@10:48:15.949 spec-protocol> State 1: state invariant 26 holds. I@10:48:15.990 spec-protocol> State 1: state invariant 27 holds. I@10:48:16.011 spec-protocol> State 1: state invariant 28 holds. I@10:48:16.080 spec-protocol> State 1: state invariant 29 holds. I@10:48:16.093 spec-protocol> State 1: state invariant 30 holds. I@10:48:16.914 spec-protocol> State 1: state invariant 31 holds. I@10:48:17.248 spec-protocol> State 1: state invariant 32 holds. I@10:48:17.594 spec-protocol> State 1: Checking 26 state invariants I@10:48:18.049 spec-protocol> State 1: state invariant 0 holds. I@10:48:18.051 spec-protocol> State 1: state invariant 1 holds. I@10:48:18.084 spec-protocol> State 1: state invariant 9 holds. I@10:48:18.110 spec-protocol> State 1: state invariant 10 holds. I@10:48:18.113 spec-protocol> State 1: state invariant 12 holds. I@10:48:18.140 spec-protocol> State 1: state invariant 14 holds. I@10:48:18.154 spec-protocol> State 1: state invariant 15 holds. I@10:48:18.173 spec-protocol> State 1: state invariant 16 holds. I@10:48:18.178 spec-protocol> State 1: state invariant 17 holds. I@10:48:18.181 spec-protocol> State 1: state invariant 18 holds. I@10:48:18.203 spec-protocol> State 1: state invariant 19 holds. I@10:48:18.240 spec-protocol> State 1: state invariant 20 holds. I@10:48:18.284 spec-protocol> State 1: state invariant 21 holds. I@10:48:18.325 spec-protocol> State 1: state invariant 22 holds. I@10:48:18.347 spec-protocol> State 1: state invariant 23 holds. I@10:48:18.360 spec-protocol> State 1: state invariant 24 holds. I@10:48:18.364 spec-protocol> State 1: state invariant 26 holds. I@10:48:18.370 spec-protocol> State 1: state invariant 27 holds. I@10:48:18.392 spec-protocol> State 1: state invariant 28 holds. I@10:48:18.437 spec-protocol> State 1: state invariant 29 holds. I@10:48:18.448 spec-protocol> State 1: state invariant 30 holds. I@10:48:18.688 spec-protocol> State 1: state invariant 31 holds. I@10:48:18.908 spec-protocol> State 1: state invariant 32 holds. I@10:48:19.307 spec-protocol> State 1: state invariant 33 holds. I@10:48:19.323 spec-protocol> State 1: state invariant 34 holds. I@10:48:19.345 spec-protocol> State 1: state invariant 35 holds. I@10:48:19.369 spec-protocol> State 1: Checking 22 state invariants I@10:48:19.839 spec-protocol> State 1: state invariant 0 holds. I@10:48:19.843 spec-protocol> State 1: state invariant 1 holds. I@10:48:19.895 spec-protocol> State 1: state invariant 9 holds. I@10:48:19.921 spec-protocol> State 1: state invariant 10 holds. I@10:48:19.928 spec-protocol> State 1: state invariant 12 holds. I@10:48:19.960 spec-protocol> State 1: state invariant 14 holds. I@10:48:19.980 spec-protocol> State 1: state invariant 15 holds. I@10:48:19.999 spec-protocol> State 1: state invariant 16 holds. I@10:48:20.008 spec-protocol> State 1: state invariant 17 holds. I@10:48:20.015 spec-protocol> State 1: state invariant 18 holds. I@10:48:20.048 spec-protocol> State 1: state invariant 19 holds. I@10:48:20.111 spec-protocol> State 1: state invariant 20 holds. I@10:48:20.149 spec-protocol> State 1: state invariant 21 holds. I@10:48:20.231 spec-protocol> State 1: state invariant 23 holds. I@10:48:20.253 spec-protocol> State 1: state invariant 24 holds. I@10:48:20.265 spec-protocol> State 1: state invariant 26 holds. I@10:48:20.303 spec-protocol> State 1: state invariant 27 holds. I@10:48:20.437 spec-protocol> State 1: state invariant 28 holds. I@10:48:20.547 spec-protocol> State 1: state invariant 29 holds. I@10:48:20.560 spec-protocol> State 1: state invariant 30 holds. I@10:48:20.797 spec-protocol> State 1: state invariant 31 holds. I@10:48:21.021 spec-protocol> State 1: state invariant 32 holds. I@10:48:21.258 spec-protocol> Step 1: Transition #16 is disabled I@10:48:21.316 spec-protocol> State 1: Checking 21 state invariants I@10:48:21.473 spec-protocol> State 1: state invariant 0 holds. I@10:48:21.478 spec-protocol> State 1: state invariant 1 holds. I@10:48:21.514 spec-protocol> State 1: state invariant 9 holds. I@10:48:21.532 spec-protocol> State 1: state invariant 10 holds. I@10:48:21.537 spec-protocol> State 1: state invariant 12 holds. I@10:48:21.551 spec-protocol> State 1: state invariant 14 holds. I@10:48:21.562 spec-protocol> State 1: state invariant 15 holds. I@10:48:21.585 spec-protocol> State 1: state invariant 17 holds. I@10:48:21.589 spec-protocol> State 1: state invariant 18 holds. I@10:48:21.613 spec-protocol> State 1: state invariant 19 holds. I@10:48:21.658 spec-protocol> State 1: state invariant 20 holds. I@10:48:21.683 spec-protocol> State 1: state invariant 21 holds. I@10:48:21.854 spec-protocol> State 1: state invariant 23 holds. I@10:48:21.867 spec-protocol> State 1: state invariant 24 holds. I@10:48:21.872 spec-protocol> State 1: state invariant 26 holds. I@10:48:21.879 spec-protocol> State 1: state invariant 27 holds. I@10:48:21.913 spec-protocol> State 1: state invariant 28 holds. I@10:48:21.981 spec-protocol> State 1: state invariant 29 holds. I@10:48:21.995 spec-protocol> State 1: state invariant 30 holds. I@10:48:22.437 spec-protocol> State 1: state invariant 31 holds. I@10:48:22.747 spec-protocol> State 1: state invariant 32 holds. I@10:48:22.956 spec-protocol> Step 1: Transition #18 is disabled I@10:48:22.999 spec-protocol> State 1: Checking 21 state invariants I@10:48:23.064 spec-protocol> State 1: state invariant 0 holds. I@10:48:23.066 spec-protocol> State 1: state invariant 1 holds. I@10:48:23.097 spec-protocol> State 1: state invariant 9 holds. I@10:48:23.110 spec-protocol> State 1: state invariant 10 holds. I@10:48:23.114 spec-protocol> State 1: state invariant 12 holds. I@10:48:23.122 spec-protocol> State 1: state invariant 14 holds. I@10:48:23.132 spec-protocol> State 1: state invariant 15 holds. I@10:48:23.140 spec-protocol> State 1: state invariant 17 holds. I@10:48:23.143 spec-protocol> State 1: state invariant 18 holds. I@10:48:23.172 spec-protocol> State 1: state invariant 19 holds. I@10:48:23.200 spec-protocol> State 1: state invariant 20 holds. I@10:48:23.222 spec-protocol> State 1: state invariant 21 holds. I@10:48:23.251 spec-protocol> State 1: state invariant 23 holds. I@10:48:23.263 spec-protocol> State 1: state invariant 24 holds. I@10:48:23.266 spec-protocol> State 1: state invariant 26 holds. I@10:48:23.272 spec-protocol> State 1: state invariant 27 holds. I@10:48:23.328 spec-protocol> State 1: state invariant 28 holds. I@10:48:23.403 spec-protocol> State 1: state invariant 29 holds. I@10:48:23.413 spec-protocol> State 1: state invariant 30 holds. I@10:48:23.846 spec-protocol> State 1: state invariant 31 holds. I@10:48:24.363 spec-protocol> State 1: state invariant 32 holds. I@10:48:24.795 spec-protocol> Step 1: Transition #20 is disabled I@10:48:24.848 spec-protocol> Step 1: Transition #21 is disabled I@10:48:25.034 spec-protocol> State 1: Checking 14 state invariants I@10:48:25.168 spec-protocol> State 1: state invariant 6 holds. I@10:48:25.170 spec-protocol> State 1: state invariant 7 holds. I@10:48:25.174 spec-protocol> State 1: state invariant 22 holds. I@10:48:25.205 spec-protocol> State 1: state invariant 25 holds. I@10:48:25.241 spec-protocol> State 1: state invariant 27 holds. I@10:48:25.347 spec-protocol> State 1: state invariant 28 holds. I@10:48:25.417 spec-protocol> State 1: state invariant 29 holds. I@10:48:25.427 spec-protocol> State 1: state invariant 30 holds. I@10:48:25.743 spec-protocol> State 1: state invariant 31 holds. I@10:48:25.887 spec-protocol> State 1: state invariant 32 holds. I@10:48:26.062 spec-protocol> State 1: state invariant 33 holds. I@10:48:26.072 spec-protocol> State 1: state invariant 34 holds. I@10:48:26.080 spec-protocol> State 1: state invariant 35 holds. I@10:48:26.089 spec-protocol> State 1: state invariant 38 holds. I@10:48:26.093 spec-protocol> State 1: Checking 17 state invariants I@10:48:26.213 spec-protocol> State 1: state invariant 3 holds. I@10:48:26.225 spec-protocol> State 1: state invariant 4 holds. I@10:48:26.280 spec-protocol> State 1: state invariant 5 holds. I@10:48:26.328 spec-protocol> State 1: state invariant 6 holds. I@10:48:26.332 spec-protocol> State 1: state invariant 7 holds. I@10:48:26.334 spec-protocol> State 1: state invariant 22 holds. I@10:48:26.389 spec-protocol> State 1: state invariant 25 holds. I@10:48:26.392 spec-protocol> State 1: state invariant 27 holds. I@10:48:26.398 spec-protocol> State 1: state invariant 28 holds. I@10:48:26.544 spec-protocol> State 1: state invariant 29 holds. I@10:48:26.553 spec-protocol> State 1: state invariant 30 holds. I@10:48:27.304 spec-protocol> State 1: state invariant 31 holds. I@10:48:27.790 spec-protocol> State 1: state invariant 32 holds. I@10:48:28.360 spec-protocol> State 1: state invariant 33 holds. I@10:48:28.391 spec-protocol> State 1: state invariant 34 holds. I@10:48:28.400 spec-protocol> State 1: state invariant 35 holds. I@10:48:28.408 spec-protocol> State 1: state invariant 38 holds. I@10:48:28.412 spec-protocol> Step 1: picking a transition out of 17 transition(s) I@10:48:28.416 spec-protocol> The outcome is: NoError I@10:48:28.625 spec-protocol> > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... spec-protocol> PASS #0: SanyParser I@10:48:28.884 spec-protocol> PASS #1: TypeCheckerSnowcat I@10:48:28.999 spec-protocol> > Running Snowcat .::. I@10:48:28.999 spec-protocol> > Your types are purrfect! I@10:48:34.478 spec-protocol> > All expressions are typed I@10:48:34.478 spec-protocol> PASS #2: ConfigurationPass I@10:48:34.487 spec-protocol> > Set the initialization predicate to q::inductiveInv I@10:48:34.488 spec-protocol> > Set the transition predicate to q::step I@10:48:34.488 spec-protocol> > Set an invariant to q::inv I@10:48:34.488 spec-protocol> PASS #3: DesugarerPass I@10:48:34.492 spec-protocol> > Desugaring... I@10:48:34.492 spec-protocol> PASS #4: InlinePass I@10:48:34.494 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@10:48:34.494 spec-protocol> PASS #5: TemporalPass I@10:48:34.564 spec-protocol> > Rewriting temporal operators... I@10:48:34.564 spec-protocol> > No temporal property specified, nothing to encode I@10:48:34.564 spec-protocol> PASS #6: InlinePass I@10:48:34.564 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@10:48:34.564 spec-protocol> PASS #7: PrimingPass I@10:48:34.595 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@10:48:34.596 spec-protocol> PASS #8: VCGen I@10:48:34.615 spec-protocol> > Producing verification conditions from the invariant q::inv I@10:48:34.615 spec-protocol> > VCGen produced 5 verification condition(s) I@10:48:34.616 spec-protocol> PASS #9: PreprocessingPass I@10:48:34.616 spec-protocol> > Before preprocessing: unique renaming I@10:48:34.616 spec-protocol> > Applying standard transformations: I@10:48:34.616 spec-protocol> > PrimePropagation I@10:48:34.616 spec-protocol> > Desugarer I@10:48:34.631 spec-protocol> > UniqueRenamer I@10:48:34.641 spec-protocol> > Normalizer I@10:48:34.672 spec-protocol> > Keramelizer I@10:48:34.697 spec-protocol> > After preprocessing: UniqueRenamer I@10:48:34.736 spec-protocol> PASS #10: TransitionFinderPass I@10:48:34.849 spec-protocol> > Found 1 initializing transitions I@10:48:34.854 spec-protocol> > Found 24 transitions I@10:48:34.876 spec-protocol> > No constant initializer I@10:48:34.877 spec-protocol> > Applying unique renaming I@10:48:34.877 spec-protocol> PASS #11: OptimizationPass I@10:48:34.925 spec-protocol> > Applying optimizations: I@10:48:34.925 spec-protocol> > ConstSimplifier I@10:48:34.925 spec-protocol> > ExprOptimizer I@10:48:35.018 spec-protocol> > SetMembershipSimplifier I@10:48:35.071 spec-protocol> > ConstSimplifier I@10:48:35.088 spec-protocol> PASS #12: AnalysisPass I@10:48:35.180 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@10:48:35.180 spec-protocol> > Skolemization I@10:48:35.180 spec-protocol> > Expansion I@10:48:35.186 spec-protocol> > Remove unused let-in defs I@10:48:35.211 spec-protocol> > Running analyzers... I@10:48:35.222 spec-protocol> > Introduced expression grades I@10:48:35.224 spec-protocol> PASS #13: BoundedChecker I@10:48:35.225 spec-protocol> State 0: Checking 5 state invariants I@10:48:36.941 spec-protocol> State 0: state invariant 0 holds. I@10:48:36.943 spec-protocol> State 0: state invariant 1 holds. I@10:48:36.945 spec-protocol> State 0: state invariant 2 holds. I@10:48:36.949 spec-protocol> State 0: state invariant 3 holds. I@10:48:36.958 spec-protocol> State 0: state invariant 4 holds. I@10:48:37.034 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@10:48:37.038 spec-protocol> The outcome is: NoError I@10:48:37.072 spec-protocol> [ok] No violation found (121928ms). 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