this derivation will be built: /nix/store/f0df4i332h0ffnicr5r6j99lh8jxgfwh-spec-protocol.drv these 2 paths will be fetched (211.6 MiB download, 342.5 MiB unpacked): /nix/store/ldr6rmj403iklkgz0divz52nxm60286c-quint-0.33.0 /nix/store/01ybz5s53dwflmbrs5qncy3pdh80m3vg-quint-cli-0.33.0 building '/nix/store/f0df4i332h0ffnicr5r6j99lh8jxgfwh-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-25T16-54-06_9433390518880753966 spec-protocol> # APALACHE version: 0.62.1 | build: a321771 I@16:54:06.710 spec-protocol> Starting checker server on port 8822... I@16:54:06.714 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: b3:c5:af:d6:fe:fe:24:16 W@16:54:07.484 spec-protocol> Oct 25, 2026 4:54:10 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:54:10.901 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:54:11.626 spec-protocol> > Running Snowcat .::. I@16:54:11.626 spec-protocol> > Your types are purrfect! I@16:54:13.885 spec-protocol> > All expressions are typed I@16:54:13.886 spec-protocol> PASS #2: ConfigurationPass I@16:54:13.887 spec-protocol> > Set the initialization predicate to q::init I@16:54:13.892 spec-protocol> > Set the transition predicate to q::step I@16:54:13.892 spec-protocol> > Set an invariant to q::inductiveInv I@16:54:13.892 spec-protocol> PASS #3: DesugarerPass I@16:54:13.899 spec-protocol> > Desugaring... I@16:54:13.900 spec-protocol> PASS #4: InlinePass I@16:54:13.915 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:13.915 spec-protocol> PASS #5: TemporalPass I@16:54:14.019 spec-protocol> > Rewriting temporal operators... I@16:54:14.019 spec-protocol> > No temporal property specified, nothing to encode I@16:54:14.019 spec-protocol> PASS #6: InlinePass I@16:54:14.019 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:14.019 spec-protocol> PASS #7: PrimingPass I@16:54:14.045 spec-protocol> > Introducing q::initPrimed for q::init' I@16:54:14.048 spec-protocol> PASS #8: VCGen I@16:54:14.049 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@16:54:14.049 spec-protocol> > VCGen produced 39 verification condition(s) I@16:54:14.058 spec-protocol> PASS #9: PreprocessingPass I@16:54:14.064 spec-protocol> > Before preprocessing: unique renaming I@16:54:14.064 spec-protocol> > Applying standard transformations: I@16:54:14.072 spec-protocol> > PrimePropagation I@16:54:14.072 spec-protocol> > Desugarer I@16:54:14.080 spec-protocol> > UniqueRenamer I@16:54:14.088 spec-protocol> > Normalizer I@16:54:14.115 spec-protocol> > SetMembershipSimplifier I@16:54:14.135 spec-protocol> > Keramelizer I@16:54:14.145 spec-protocol> > After preprocessing: UniqueRenamer I@16:54:14.168 spec-protocol> PASS #10: TransitionFinderPass I@16:54:14.211 spec-protocol> > Found 1 initializing transitions I@16:54:14.225 spec-protocol> > Found 24 transitions I@16:54:14.259 spec-protocol> > No constant initializer I@16:54:14.259 spec-protocol> > Applying unique renaming I@16:54:14.261 spec-protocol> PASS #11: OptimizationPass I@16:54:14.289 spec-protocol> > Applying optimizations: I@16:54:14.294 spec-protocol> > ConstSimplifier I@16:54:14.294 spec-protocol> > ExprOptimizer I@16:54:14.366 spec-protocol> > SetMembershipSimplifier I@16:54:14.390 spec-protocol> > ConstSimplifier I@16:54:14.397 spec-protocol> PASS #12: AnalysisPass I@16:54:14.468 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:54:14.471 spec-protocol> > Skolemization I@16:54:14.471 spec-protocol> > Expansion I@16:54:14.476 spec-protocol> > Remove unused let-in defs I@16:54:14.495 spec-protocol> > Running analyzers... I@16:54:14.507 spec-protocol> > Introduced expression grades I@16:54:14.517 spec-protocol> PASS #13: BoundedChecker I@16:54:14.517 spec-protocol> State 0: Checking 39 state invariants I@16:54:15.007 spec-protocol> State 0: state invariant 0 holds. I@16:54:15.014 spec-protocol> State 0: state invariant 1 holds. I@16:54:15.068 spec-protocol> State 0: state invariant 2 holds. I@16:54:15.069 spec-protocol> State 0: state invariant 3 holds. I@16:54:15.070 spec-protocol> State 0: state invariant 4 holds. I@16:54:15.109 spec-protocol> State 0: state invariant 5 holds. I@16:54:15.114 spec-protocol> State 0: state invariant 6 holds. I@16:54:15.116 spec-protocol> State 0: state invariant 7 holds. I@16:54:15.117 spec-protocol> State 0: state invariant 8 holds. I@16:54:15.118 spec-protocol> State 0: state invariant 9 holds. I@16:54:15.126 spec-protocol> State 0: state invariant 10 holds. I@16:54:15.127 spec-protocol> State 0: state invariant 11 holds. I@16:54:15.127 spec-protocol> State 0: state invariant 12 holds. I@16:54:15.137 spec-protocol> State 0: state invariant 13 holds. I@16:54:15.138 spec-protocol> State 0: state invariant 14 holds. I@16:54:15.146 spec-protocol> State 0: state invariant 15 holds. I@16:54:15.147 spec-protocol> State 0: state invariant 16 holds. I@16:54:15.148 spec-protocol> State 0: state invariant 17 holds. I@16:54:15.148 spec-protocol> State 0: state invariant 18 holds. I@16:54:15.151 spec-protocol> State 0: state invariant 19 holds. I@16:54:15.156 spec-protocol> State 0: state invariant 20 holds. I@16:54:15.166 spec-protocol> State 0: state invariant 21 holds. I@16:54:15.175 spec-protocol> State 0: state invariant 22 holds. I@16:54:15.180 spec-protocol> State 0: state invariant 23 holds. I@16:54:15.191 spec-protocol> State 0: state invariant 24 holds. I@16:54:15.195 spec-protocol> State 0: state invariant 25 holds. I@16:54:15.196 spec-protocol> State 0: state invariant 26 holds. I@16:54:15.202 spec-protocol> State 0: state invariant 27 holds. I@16:54:15.214 spec-protocol> State 0: state invariant 28 holds. I@16:54:15.233 spec-protocol> State 0: state invariant 29 holds. I@16:54:15.241 spec-protocol> State 0: state invariant 30 holds. I@16:54:15.263 spec-protocol> State 0: state invariant 31 holds. I@16:54:15.299 spec-protocol> State 0: state invariant 32 holds. I@16:54:15.328 spec-protocol> State 0: state invariant 33 holds. I@16:54:15.329 spec-protocol> State 0: state invariant 34 holds. I@16:54:15.334 spec-protocol> State 0: state invariant 35 holds. I@16:54:15.339 spec-protocol> State 0: state invariant 36 holds. I@16:54:15.341 spec-protocol> State 0: state invariant 37 holds. I@16:54:15.342 spec-protocol> State 0: state invariant 38 holds. I@16:54:15.342 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:54:15.343 spec-protocol> The outcome is: NoError I@16:54:15.351 spec-protocol> > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... spec-protocol> PASS #0: SanyParser I@16:54:15.670 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:54:15.824 spec-protocol> > Running Snowcat .::. I@16:54:15.824 spec-protocol> > Your types are purrfect! I@16:54:18.418 spec-protocol> > All expressions are typed I@16:54:18.419 spec-protocol> PASS #2: ConfigurationPass I@16:54:18.419 spec-protocol> > Set the initialization predicate to q::inductiveInv I@16:54:18.419 spec-protocol> > Set the transition predicate to q::step I@16:54:18.420 spec-protocol> > Set an invariant to q::inductiveInv I@16:54:18.420 spec-protocol> PASS #3: DesugarerPass I@16:54:18.422 spec-protocol> > Desugaring... I@16:54:18.422 spec-protocol> PASS #4: InlinePass I@16:54:18.424 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:18.424 spec-protocol> PASS #5: TemporalPass I@16:54:18.454 spec-protocol> > Rewriting temporal operators... I@16:54:18.454 spec-protocol> > No temporal property specified, nothing to encode I@16:54:18.454 spec-protocol> PASS #6: InlinePass I@16:54:18.455 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:18.455 spec-protocol> PASS #7: PrimingPass I@16:54:18.465 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:18.465 spec-protocol> PASS #8: VCGen I@16:54:18.466 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@16:54:18.466 spec-protocol> > VCGen produced 39 verification condition(s) I@16:54:18.467 spec-protocol> PASS #9: PreprocessingPass I@16:54:18.469 spec-protocol> > Before preprocessing: unique renaming I@16:54:18.469 spec-protocol> > Applying standard transformations: I@16:54:18.469 spec-protocol> > PrimePropagation I@16:54:18.470 spec-protocol> > Desugarer I@16:54:18.472 spec-protocol> > UniqueRenamer I@16:54:18.476 spec-protocol> > Normalizer I@16:54:18.487 spec-protocol> > SetMembershipSimplifier I@16:54:18.503 spec-protocol> > Keramelizer I@16:54:18.506 spec-protocol> > After preprocessing: UniqueRenamer I@16:54:18.516 spec-protocol> PASS #10: TransitionFinderPass I@16:54:18.530 spec-protocol> > Found 1 initializing transitions I@16:54:18.533 spec-protocol> > Found 24 transitions I@16:54:18.543 spec-protocol> > No constant initializer I@16:54:18.543 spec-protocol> > Applying unique renaming I@16:54:18.544 spec-protocol> PASS #11: OptimizationPass I@16:54:18.566 spec-protocol> > Applying optimizations: I@16:54:18.566 spec-protocol> > ConstSimplifier I@16:54:18.566 spec-protocol> > ExprOptimizer I@16:54:18.648 spec-protocol> > SetMembershipSimplifier I@16:54:18.661 spec-protocol> > ConstSimplifier I@16:54:18.665 spec-protocol> PASS #12: AnalysisPass I@16:54:18.739 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:54:18.739 spec-protocol> > Skolemization I@16:54:18.739 spec-protocol> > Expansion I@16:54:18.743 spec-protocol> > Remove unused let-in defs I@16:54:18.756 spec-protocol> > Running analyzers... I@16:54:18.760 spec-protocol> > Introduced expression grades I@16:54:18.762 spec-protocol> PASS #13: BoundedChecker I@16:54:18.762 spec-protocol> State 0: Checking 39 state invariants I@16:54:19.497 spec-protocol> State 0: state invariant 0 holds. I@16:54:19.503 spec-protocol> State 0: state invariant 1 holds. I@16:54:19.531 spec-protocol> State 0: state invariant 2 holds. I@16:54:19.535 spec-protocol> State 0: state invariant 3 holds. I@16:54:19.537 spec-protocol> State 0: state invariant 4 holds. I@16:54:19.563 spec-protocol> State 0: state invariant 5 holds. I@16:54:19.574 spec-protocol> State 0: state invariant 6 holds. I@16:54:19.577 spec-protocol> State 0: state invariant 7 holds. I@16:54:19.578 spec-protocol> State 0: state invariant 8 holds. I@16:54:19.579 spec-protocol> State 0: state invariant 9 holds. I@16:54:19.581 spec-protocol> State 0: state invariant 10 holds. I@16:54:19.582 spec-protocol> State 0: state invariant 11 holds. I@16:54:19.584 spec-protocol> State 0: state invariant 12 holds. I@16:54:19.591 spec-protocol> State 0: state invariant 13 holds. I@16:54:19.594 spec-protocol> State 0: state invariant 14 holds. I@16:54:19.603 spec-protocol> State 0: state invariant 15 holds. I@16:54:19.605 spec-protocol> State 0: state invariant 16 holds. I@16:54:19.606 spec-protocol> State 0: state invariant 17 holds. I@16:54:19.607 spec-protocol> State 0: state invariant 18 holds. I@16:54:19.614 spec-protocol> State 0: state invariant 19 holds. I@16:54:19.620 spec-protocol> State 0: state invariant 20 holds. I@16:54:19.628 spec-protocol> State 0: state invariant 21 holds. I@16:54:19.642 spec-protocol> State 0: state invariant 22 holds. I@16:54:19.652 spec-protocol> State 0: state invariant 23 holds. I@16:54:19.662 spec-protocol> State 0: state invariant 24 holds. I@16:54:19.663 spec-protocol> State 0: state invariant 25 holds. I@16:54:19.664 spec-protocol> State 0: state invariant 26 holds. I@16:54:19.666 spec-protocol> State 0: state invariant 27 holds. I@16:54:19.672 spec-protocol> State 0: state invariant 28 holds. I@16:54:19.697 spec-protocol> State 0: state invariant 29 holds. I@16:54:19.706 spec-protocol> State 0: state invariant 30 holds. I@16:54:19.835 spec-protocol> State 0: state invariant 31 holds. I@16:54:19.976 spec-protocol> State 0: state invariant 32 holds. I@16:54:20.129 spec-protocol> State 0: state invariant 33 holds. I@16:54:20.132 spec-protocol> State 0: state invariant 34 holds. I@16:54:20.138 spec-protocol> State 0: state invariant 35 holds. I@16:54:20.144 spec-protocol> State 0: state invariant 36 holds. I@16:54:20.145 spec-protocol> State 0: state invariant 37 holds. I@16:54:20.146 spec-protocol> State 0: state invariant 38 holds. I@16:54:20.147 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:54:20.148 spec-protocol> State 1: Checking 12 state invariants I@16:54:20.176 spec-protocol> State 1: state invariant 0 holds. I@16:54:20.178 spec-protocol> State 1: state invariant 1 holds. I@16:54:20.210 spec-protocol> State 1: state invariant 18 holds. I@16:54:20.220 spec-protocol> State 1: state invariant 19 holds. I@16:54:20.227 spec-protocol> State 1: state invariant 20 holds. I@16:54:20.236 spec-protocol> State 1: state invariant 21 holds. I@16:54:20.247 spec-protocol> State 1: state invariant 27 holds. I@16:54:20.258 spec-protocol> State 1: state invariant 28 holds. I@16:54:20.287 spec-protocol> State 1: state invariant 29 holds. I@16:54:20.296 spec-protocol> State 1: state invariant 30 holds. I@16:54:20.428 spec-protocol> State 1: state invariant 31 holds. I@16:54:20.562 spec-protocol> State 1: state invariant 32 holds. I@16:54:20.663 spec-protocol> State 1: Checking 4 state invariants I@16:54:20.686 spec-protocol> State 1: state invariant 13 holds. I@16:54:20.688 spec-protocol> State 1: state invariant 29 holds. I@16:54:20.694 spec-protocol> State 1: state invariant 30 holds. I@16:54:20.818 spec-protocol> State 1: state invariant 31 holds. I@16:54:20.949 spec-protocol> State 1: Checking 16 state invariants I@16:54:21.002 spec-protocol> State 1: state invariant 0 holds. I@16:54:21.003 spec-protocol> State 1: state invariant 1 holds. I@16:54:21.027 spec-protocol> State 1: state invariant 3 holds. I@16:54:21.030 spec-protocol> State 1: state invariant 4 holds. I@16:54:21.053 spec-protocol> State 1: state invariant 5 holds. I@16:54:21.062 spec-protocol> State 1: state invariant 18 holds. I@16:54:21.069 spec-protocol> State 1: state invariant 19 holds. I@16:54:21.075 spec-protocol> State 1: state invariant 20 holds. I@16:54:21.082 spec-protocol> State 1: state invariant 21 holds. I@16:54:21.090 spec-protocol> State 1: state invariant 23 holds. I@16:54:21.100 spec-protocol> State 1: state invariant 27 holds. I@16:54:21.105 spec-protocol> State 1: state invariant 28 holds. I@16:54:21.124 spec-protocol> State 1: state invariant 29 holds. I@16:54:21.132 spec-protocol> State 1: state invariant 30 holds. I@16:54:21.232 spec-protocol> State 1: state invariant 31 holds. I@16:54:21.345 spec-protocol> State 1: state invariant 32 holds. I@16:54:21.436 spec-protocol> State 1: Checking 6 state invariants I@16:54:21.455 spec-protocol> State 1: state invariant 2 holds. I@16:54:21.457 spec-protocol> State 1: state invariant 27 holds. I@16:54:21.473 spec-protocol> State 1: state invariant 29 holds. I@16:54:21.480 spec-protocol> State 1: state invariant 30 holds. I@16:54:21.729 spec-protocol> State 1: state invariant 31 holds. I@16:54:21.888 spec-protocol> State 1: state invariant 38 holds. I@16:54:21.892 spec-protocol> State 1: Checking 15 state invariants I@16:54:21.910 spec-protocol> State 1: state invariant 0 holds. I@16:54:21.911 spec-protocol> State 1: state invariant 1 holds. I@16:54:21.937 spec-protocol> State 1: state invariant 2 holds. I@16:54:21.939 spec-protocol> State 1: state invariant 12 holds. I@16:54:21.948 spec-protocol> State 1: state invariant 18 holds. I@16:54:21.956 spec-protocol> State 1: state invariant 19 holds. I@16:54:21.965 spec-protocol> State 1: state invariant 20 holds. I@16:54:21.973 spec-protocol> State 1: state invariant 21 holds. I@16:54:21.983 spec-protocol> State 1: state invariant 27 holds. I@16:54:21.992 spec-protocol> State 1: state invariant 28 holds. I@16:54:22.027 spec-protocol> State 1: state invariant 29 holds. I@16:54:22.036 spec-protocol> State 1: state invariant 30 holds. I@16:54:22.187 spec-protocol> State 1: state invariant 31 holds. I@16:54:22.326 spec-protocol> State 1: state invariant 32 holds. I@16:54:22.474 spec-protocol> State 1: state invariant 37 holds. I@16:54:22.477 spec-protocol> State 1: Checking 18 state invariants I@16:54:22.693 spec-protocol> State 1: state invariant 9 holds. I@16:54:22.698 spec-protocol> State 1: state invariant 10 holds. I@16:54:22.699 spec-protocol> State 1: state invariant 11 holds. I@16:54:22.700 spec-protocol> State 1: state invariant 14 holds. I@16:54:22.708 spec-protocol> State 1: state invariant 15 holds. I@16:54:22.710 spec-protocol> State 1: state invariant 17 holds. I@16:54:22.711 spec-protocol> State 1: state invariant 22 holds. I@16:54:22.719 spec-protocol> State 1: state invariant 24 holds. I@16:54:22.721 spec-protocol> State 1: state invariant 26 holds. I@16:54:22.723 spec-protocol> State 1: state invariant 27 holds. I@16:54:22.731 spec-protocol> State 1: state invariant 28 holds. I@16:54:22.753 spec-protocol> State 1: state invariant 29 holds. I@16:54:22.760 spec-protocol> State 1: state invariant 30 holds. I@16:54:22.816 spec-protocol> State 1: state invariant 31 holds. I@16:54:22.895 spec-protocol> State 1: state invariant 32 holds. I@16:54:23.015 spec-protocol> State 1: state invariant 33 holds. I@16:54:23.019 spec-protocol> State 1: state invariant 34 holds. I@16:54:23.025 spec-protocol> State 1: state invariant 35 holds. I@16:54:23.041 spec-protocol> State 1: Checking 14 state invariants I@16:54:23.273 spec-protocol> State 1: state invariant 9 holds. I@16:54:23.277 spec-protocol> State 1: state invariant 10 holds. I@16:54:23.279 spec-protocol> State 1: state invariant 11 holds. I@16:54:23.280 spec-protocol> State 1: state invariant 14 holds. I@16:54:23.288 spec-protocol> State 1: state invariant 15 holds. I@16:54:23.290 spec-protocol> State 1: state invariant 17 holds. I@16:54:23.291 spec-protocol> State 1: state invariant 24 holds. I@16:54:23.293 spec-protocol> State 1: state invariant 26 holds. I@16:54:23.295 spec-protocol> State 1: state invariant 27 holds. I@16:54:23.301 spec-protocol> State 1: state invariant 28 holds. I@16:54:23.315 spec-protocol> State 1: state invariant 29 holds. I@16:54:23.322 spec-protocol> State 1: state invariant 30 holds. I@16:54:23.378 spec-protocol> State 1: state invariant 31 holds. I@16:54:23.452 spec-protocol> State 1: state invariant 32 holds. I@16:54:23.515 spec-protocol> State 1: Checking 26 state invariants I@16:54:23.640 spec-protocol> State 1: state invariant 0 holds. I@16:54:23.641 spec-protocol> State 1: state invariant 1 holds. I@16:54:23.665 spec-protocol> State 1: state invariant 9 holds. I@16:54:23.672 spec-protocol> State 1: state invariant 10 holds. I@16:54:23.674 spec-protocol> State 1: state invariant 11 holds. I@16:54:23.675 spec-protocol> State 1: state invariant 12 holds. I@16:54:23.682 spec-protocol> State 1: state invariant 14 holds. I@16:54:23.693 spec-protocol> State 1: state invariant 15 holds. I@16:54:23.697 spec-protocol> State 1: state invariant 17 holds. I@16:54:23.699 spec-protocol> State 1: state invariant 18 holds. I@16:54:23.708 spec-protocol> State 1: state invariant 19 holds. I@16:54:23.719 spec-protocol> State 1: state invariant 20 holds. I@16:54:23.727 spec-protocol> State 1: state invariant 21 holds. I@16:54:23.741 spec-protocol> State 1: state invariant 22 holds. I@16:54:23.749 spec-protocol> State 1: state invariant 23 holds. I@16:54:23.758 spec-protocol> State 1: state invariant 24 holds. I@16:54:23.760 spec-protocol> State 1: state invariant 26 holds. I@16:54:23.764 spec-protocol> State 1: state invariant 27 holds. I@16:54:23.784 spec-protocol> State 1: state invariant 28 holds. I@16:54:23.820 spec-protocol> State 1: state invariant 29 holds. I@16:54:23.829 spec-protocol> State 1: state invariant 30 holds. I@16:54:24.005 spec-protocol> State 1: state invariant 31 holds. I@16:54:24.160 spec-protocol> State 1: state invariant 32 holds. I@16:54:24.345 spec-protocol> State 1: state invariant 33 holds. I@16:54:24.349 spec-protocol> State 1: state invariant 34 holds. I@16:54:24.359 spec-protocol> State 1: state invariant 35 holds. I@16:54:24.371 spec-protocol> State 1: Checking 22 state invariants I@16:54:24.503 spec-protocol> State 1: state invariant 0 holds. I@16:54:24.504 spec-protocol> State 1: state invariant 1 holds. I@16:54:24.528 spec-protocol> State 1: state invariant 9 holds. I@16:54:24.536 spec-protocol> State 1: state invariant 10 holds. I@16:54:24.538 spec-protocol> State 1: state invariant 11 holds. I@16:54:24.540 spec-protocol> State 1: state invariant 12 holds. I@16:54:24.546 spec-protocol> State 1: state invariant 14 holds. I@16:54:24.558 spec-protocol> State 1: state invariant 15 holds. I@16:54:24.564 spec-protocol> State 1: state invariant 17 holds. I@16:54:24.567 spec-protocol> State 1: state invariant 18 holds. I@16:54:24.574 spec-protocol> State 1: state invariant 19 holds. I@16:54:24.592 spec-protocol> State 1: state invariant 20 holds. I@16:54:24.603 spec-protocol> State 1: state invariant 21 holds. I@16:54:24.614 spec-protocol> State 1: state invariant 23 holds. I@16:54:24.623 spec-protocol> State 1: state invariant 24 holds. I@16:54:24.625 spec-protocol> State 1: state invariant 26 holds. I@16:54:24.633 spec-protocol> State 1: state invariant 27 holds. I@16:54:24.659 spec-protocol> State 1: state invariant 28 holds. I@16:54:24.706 spec-protocol> State 1: state invariant 29 holds. I@16:54:24.715 spec-protocol> State 1: state invariant 30 holds. I@16:54:24.928 spec-protocol> State 1: state invariant 31 holds. I@16:54:25.087 spec-protocol> State 1: state invariant 32 holds. I@16:54:25.237 spec-protocol> Step 1: Transition #10 is disabled I@16:54:25.276 spec-protocol> Step 1: Transition #11 is disabled I@16:54:25.316 spec-protocol> State 1: Checking 27 state invariants I@16:54:25.455 spec-protocol> State 1: state invariant 0 holds. I@16:54:25.457 spec-protocol> State 1: state invariant 1 holds. I@16:54:25.480 spec-protocol> State 1: state invariant 9 holds. I@16:54:25.488 spec-protocol> State 1: state invariant 10 holds. I@16:54:25.490 spec-protocol> State 1: state invariant 12 holds. I@16:54:25.496 spec-protocol> State 1: state invariant 13 holds. I@16:54:25.497 spec-protocol> State 1: state invariant 14 holds. I@16:54:25.505 spec-protocol> State 1: state invariant 15 holds. I@16:54:25.519 spec-protocol> State 1: state invariant 16 holds. I@16:54:25.520 spec-protocol> State 1: state invariant 17 holds. I@16:54:25.522 spec-protocol> State 1: state invariant 18 holds. I@16:54:25.528 spec-protocol> State 1: state invariant 19 holds. I@16:54:25.539 spec-protocol> State 1: state invariant 20 holds. I@16:54:25.550 spec-protocol> State 1: state invariant 21 holds. I@16:54:25.561 spec-protocol> State 1: state invariant 22 holds. I@16:54:25.572 spec-protocol> State 1: state invariant 23 holds. I@16:54:25.581 spec-protocol> State 1: state invariant 24 holds. I@16:54:25.583 spec-protocol> State 1: state invariant 26 holds. I@16:54:25.586 spec-protocol> State 1: state invariant 27 holds. I@16:54:25.607 spec-protocol> State 1: state invariant 28 holds. I@16:54:25.633 spec-protocol> State 1: state invariant 29 holds. I@16:54:25.641 spec-protocol> State 1: state invariant 30 holds. I@16:54:25.765 spec-protocol> State 1: state invariant 31 holds. I@16:54:25.907 spec-protocol> State 1: state invariant 32 holds. I@16:54:26.026 spec-protocol> State 1: state invariant 33 holds. I@16:54:26.031 spec-protocol> State 1: state invariant 34 holds. I@16:54:26.038 spec-protocol> State 1: state invariant 35 holds. I@16:54:26.048 spec-protocol> State 1: Checking 23 state invariants I@16:54:26.314 spec-protocol> State 1: state invariant 0 holds. I@16:54:26.316 spec-protocol> State 1: state invariant 1 holds. I@16:54:26.341 spec-protocol> State 1: state invariant 9 holds. I@16:54:26.351 spec-protocol> State 1: state invariant 10 holds. I@16:54:26.353 spec-protocol> State 1: state invariant 12 holds. I@16:54:26.360 spec-protocol> State 1: state invariant 13 holds. I@16:54:26.361 spec-protocol> State 1: state invariant 14 holds. I@16:54:26.369 spec-protocol> State 1: state invariant 15 holds. I@16:54:26.374 spec-protocol> State 1: state invariant 16 holds. I@16:54:26.375 spec-protocol> State 1: state invariant 17 holds. I@16:54:26.376 spec-protocol> State 1: state invariant 18 holds. I@16:54:26.382 spec-protocol> State 1: state invariant 19 holds. I@16:54:26.400 spec-protocol> State 1: state invariant 20 holds. I@16:54:26.407 spec-protocol> State 1: state invariant 21 holds. I@16:54:26.420 spec-protocol> State 1: state invariant 23 holds. I@16:54:26.429 spec-protocol> State 1: state invariant 24 holds. I@16:54:26.431 spec-protocol> State 1: state invariant 26 holds. I@16:54:26.437 spec-protocol> State 1: state invariant 27 holds. I@16:54:26.446 spec-protocol> State 1: state invariant 28 holds. I@16:54:26.468 spec-protocol> State 1: state invariant 29 holds. I@16:54:26.476 spec-protocol> State 1: state invariant 30 holds. I@16:54:26.647 spec-protocol> State 1: state invariant 31 holds. I@16:54:26.809 spec-protocol> State 1: state invariant 32 holds. I@16:54:26.922 spec-protocol> State 1: Checking 26 state invariants I@16:54:27.164 spec-protocol> State 1: state invariant 0 holds. I@16:54:27.167 spec-protocol> State 1: state invariant 1 holds. I@16:54:27.193 spec-protocol> State 1: state invariant 9 holds. I@16:54:27.208 spec-protocol> State 1: state invariant 10 holds. I@16:54:27.210 spec-protocol> State 1: state invariant 12 holds. I@16:54:27.219 spec-protocol> State 1: state invariant 14 holds. I@16:54:27.227 spec-protocol> State 1: state invariant 15 holds. I@16:54:27.229 spec-protocol> State 1: state invariant 16 holds. I@16:54:27.230 spec-protocol> State 1: state invariant 17 holds. I@16:54:27.232 spec-protocol> State 1: state invariant 18 holds. I@16:54:27.241 spec-protocol> State 1: state invariant 19 holds. I@16:54:27.256 spec-protocol> State 1: state invariant 20 holds. I@16:54:27.266 spec-protocol> State 1: state invariant 21 holds. I@16:54:27.291 spec-protocol> State 1: state invariant 22 holds. I@16:54:27.306 spec-protocol> State 1: state invariant 23 holds. I@16:54:27.315 spec-protocol> State 1: state invariant 24 holds. I@16:54:27.317 spec-protocol> State 1: state invariant 26 holds. I@16:54:27.322 spec-protocol> State 1: state invariant 27 holds. I@16:54:27.338 spec-protocol> State 1: state invariant 28 holds. I@16:54:27.368 spec-protocol> State 1: state invariant 29 holds. I@16:54:27.376 spec-protocol> State 1: state invariant 30 holds. I@16:54:27.507 spec-protocol> State 1: state invariant 31 holds. I@16:54:27.641 spec-protocol> State 1: state invariant 32 holds. I@16:54:27.824 spec-protocol> State 1: state invariant 33 holds. I@16:54:27.834 spec-protocol> State 1: state invariant 34 holds. I@16:54:27.845 spec-protocol> State 1: state invariant 35 holds. I@16:54:27.867 spec-protocol> State 1: Checking 22 state invariants I@16:54:28.127 spec-protocol> State 1: state invariant 0 holds. I@16:54:28.128 spec-protocol> State 1: state invariant 1 holds. I@16:54:28.157 spec-protocol> State 1: state invariant 9 holds. I@16:54:28.164 spec-protocol> State 1: state invariant 10 holds. I@16:54:28.165 spec-protocol> State 1: state invariant 12 holds. I@16:54:28.172 spec-protocol> State 1: state invariant 14 holds. I@16:54:28.180 spec-protocol> State 1: state invariant 15 holds. I@16:54:28.189 spec-protocol> State 1: state invariant 16 holds. I@16:54:28.190 spec-protocol> State 1: state invariant 17 holds. I@16:54:28.192 spec-protocol> State 1: state invariant 18 holds. I@16:54:28.198 spec-protocol> State 1: state invariant 19 holds. I@16:54:28.207 spec-protocol> State 1: state invariant 20 holds. I@16:54:28.213 spec-protocol> State 1: state invariant 21 holds. I@16:54:28.226 spec-protocol> State 1: state invariant 23 holds. I@16:54:28.234 spec-protocol> State 1: state invariant 24 holds. I@16:54:28.236 spec-protocol> State 1: state invariant 26 holds. I@16:54:28.243 spec-protocol> State 1: state invariant 27 holds. I@16:54:28.259 spec-protocol> State 1: state invariant 28 holds. I@16:54:28.281 spec-protocol> State 1: state invariant 29 holds. I@16:54:28.289 spec-protocol> State 1: state invariant 30 holds. I@16:54:28.407 spec-protocol> State 1: state invariant 31 holds. I@16:54:28.510 spec-protocol> State 1: state invariant 32 holds. I@16:54:28.614 spec-protocol> Step 1: Transition #16 is disabled I@16:54:28.701 spec-protocol> State 1: Checking 21 state invariants I@16:54:28.817 spec-protocol> State 1: state invariant 0 holds. I@16:54:28.819 spec-protocol> State 1: state invariant 1 holds. I@16:54:28.851 spec-protocol> State 1: state invariant 9 holds. I@16:54:28.863 spec-protocol> State 1: state invariant 10 holds. I@16:54:28.866 spec-protocol> State 1: state invariant 12 holds. I@16:54:28.873 spec-protocol> State 1: state invariant 14 holds. I@16:54:28.882 spec-protocol> State 1: state invariant 15 holds. I@16:54:28.892 spec-protocol> State 1: state invariant 17 holds. I@16:54:28.894 spec-protocol> State 1: state invariant 18 holds. I@16:54:28.911 spec-protocol> State 1: state invariant 19 holds. I@16:54:28.926 spec-protocol> State 1: state invariant 20 holds. I@16:54:28.939 spec-protocol> State 1: state invariant 21 holds. I@16:54:28.958 spec-protocol> State 1: state invariant 23 holds. I@16:54:28.968 spec-protocol> State 1: state invariant 24 holds. I@16:54:28.971 spec-protocol> State 1: state invariant 26 holds. I@16:54:28.974 spec-protocol> State 1: state invariant 27 holds. I@16:54:28.989 spec-protocol> State 1: state invariant 28 holds. I@16:54:29.040 spec-protocol> State 1: state invariant 29 holds. I@16:54:29.050 spec-protocol> State 1: state invariant 30 holds. I@16:54:29.221 spec-protocol> State 1: state invariant 31 holds. I@16:54:29.385 spec-protocol> State 1: state invariant 32 holds. I@16:54:29.535 spec-protocol> Step 1: Transition #18 is disabled I@16:54:29.577 spec-protocol> State 1: Checking 21 state invariants I@16:54:29.644 spec-protocol> State 1: state invariant 0 holds. I@16:54:29.646 spec-protocol> State 1: state invariant 1 holds. I@16:54:29.671 spec-protocol> State 1: state invariant 9 holds. I@16:54:29.679 spec-protocol> State 1: state invariant 10 holds. I@16:54:29.682 spec-protocol> State 1: state invariant 12 holds. I@16:54:29.689 spec-protocol> State 1: state invariant 14 holds. I@16:54:29.698 spec-protocol> State 1: state invariant 15 holds. I@16:54:29.706 spec-protocol> State 1: state invariant 17 holds. I@16:54:29.708 spec-protocol> State 1: state invariant 18 holds. I@16:54:29.718 spec-protocol> State 1: state invariant 19 holds. I@16:54:29.734 spec-protocol> State 1: state invariant 20 holds. I@16:54:29.764 spec-protocol> State 1: state invariant 21 holds. I@16:54:29.791 spec-protocol> State 1: state invariant 23 holds. I@16:54:29.801 spec-protocol> State 1: state invariant 24 holds. I@16:54:29.804 spec-protocol> State 1: state invariant 26 holds. I@16:54:29.807 spec-protocol> State 1: state invariant 27 holds. I@16:54:29.832 spec-protocol> State 1: state invariant 28 holds. I@16:54:29.879 spec-protocol> State 1: state invariant 29 holds. I@16:54:29.889 spec-protocol> State 1: state invariant 30 holds. I@16:54:30.157 spec-protocol> State 1: state invariant 31 holds. I@16:54:30.347 spec-protocol> State 1: state invariant 32 holds. I@16:54:30.501 spec-protocol> Step 1: Transition #20 is disabled I@16:54:30.540 spec-protocol> Step 1: Transition #21 is disabled I@16:54:30.602 spec-protocol> State 1: Checking 14 state invariants I@16:54:30.686 spec-protocol> State 1: state invariant 6 holds. I@16:54:30.687 spec-protocol> State 1: state invariant 7 holds. I@16:54:30.690 spec-protocol> State 1: state invariant 22 holds. I@16:54:30.702 spec-protocol> State 1: state invariant 25 holds. I@16:54:30.706 spec-protocol> State 1: state invariant 27 holds. I@16:54:30.730 spec-protocol> State 1: state invariant 28 holds. I@16:54:30.761 spec-protocol> State 1: state invariant 29 holds. I@16:54:30.769 spec-protocol> State 1: state invariant 30 holds. I@16:54:30.884 spec-protocol> State 1: state invariant 31 holds. I@16:54:30.965 spec-protocol> State 1: state invariant 32 holds. I@16:54:31.065 spec-protocol> State 1: state invariant 33 holds. I@16:54:31.071 spec-protocol> State 1: state invariant 34 holds. I@16:54:31.077 spec-protocol> State 1: state invariant 35 holds. I@16:54:31.082 spec-protocol> State 1: state invariant 38 holds. I@16:54:31.084 spec-protocol> State 1: Checking 17 state invariants I@16:54:31.167 spec-protocol> State 1: state invariant 3 holds. I@16:54:31.172 spec-protocol> State 1: state invariant 4 holds. I@16:54:31.213 spec-protocol> State 1: state invariant 5 holds. I@16:54:31.241 spec-protocol> State 1: state invariant 6 holds. I@16:54:31.244 spec-protocol> State 1: state invariant 7 holds. I@16:54:31.246 spec-protocol> State 1: state invariant 22 holds. I@16:54:31.261 spec-protocol> State 1: state invariant 25 holds. I@16:54:31.263 spec-protocol> State 1: state invariant 27 holds. I@16:54:31.269 spec-protocol> State 1: state invariant 28 holds. I@16:54:31.315 spec-protocol> State 1: state invariant 29 holds. I@16:54:31.323 spec-protocol> State 1: state invariant 30 holds. I@16:54:31.612 spec-protocol> State 1: state invariant 31 holds. I@16:54:31.818 spec-protocol> State 1: state invariant 32 holds. I@16:54:32.240 spec-protocol> State 1: state invariant 33 holds. I@16:54:32.256 spec-protocol> State 1: state invariant 34 holds. I@16:54:32.262 spec-protocol> State 1: state invariant 35 holds. I@16:54:32.267 spec-protocol> State 1: state invariant 38 holds. I@16:54:32.269 spec-protocol> Step 1: picking a transition out of 17 transition(s) I@16:54:32.270 spec-protocol> The outcome is: NoError I@16:54:32.416 spec-protocol> > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... spec-protocol> PASS #0: SanyParser I@16:54:32.626 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:54:32.705 spec-protocol> > Running Snowcat .::. I@16:54:32.705 spec-protocol> > Your types are purrfect! I@16:54:34.848 spec-protocol> > All expressions are typed I@16:54:34.849 spec-protocol> PASS #2: ConfigurationPass I@16:54:34.849 spec-protocol> > Set the initialization predicate to q::inductiveInv I@16:54:34.850 spec-protocol> > Set the transition predicate to q::step I@16:54:34.850 spec-protocol> > Set an invariant to q::inv I@16:54:34.850 spec-protocol> PASS #3: DesugarerPass I@16:54:34.852 spec-protocol> > Desugaring... I@16:54:34.852 spec-protocol> PASS #4: InlinePass I@16:54:34.853 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:54:34.853 spec-protocol> PASS #5: TemporalPass I@16:54:34.880 spec-protocol> > Rewriting temporal operators... I@16:54:34.880 spec-protocol> > No temporal property specified, nothing to encode I@16:54:34.880 spec-protocol> PASS #6: InlinePass I@16:54:34.880 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:54:34.880 spec-protocol> PASS #7: PrimingPass I@16:54:34.891 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:34.891 spec-protocol> PASS #8: VCGen I@16:54:34.892 spec-protocol> > Producing verification conditions from the invariant q::inv I@16:54:34.892 spec-protocol> > VCGen produced 5 verification condition(s) I@16:54:34.893 spec-protocol> PASS #9: PreprocessingPass I@16:54:34.893 spec-protocol> > Before preprocessing: unique renaming I@16:54:34.893 spec-protocol> > Applying standard transformations: I@16:54:34.893 spec-protocol> > PrimePropagation I@16:54:34.894 spec-protocol> > Desugarer I@16:54:34.897 spec-protocol> > UniqueRenamer I@16:54:34.904 spec-protocol> > Normalizer I@16:54:34.914 spec-protocol> > SetMembershipSimplifier I@16:54:34.919 spec-protocol> > Keramelizer I@16:54:34.922 spec-protocol> > After preprocessing: UniqueRenamer I@16:54:34.929 spec-protocol> PASS #10: TransitionFinderPass I@16:54:34.942 spec-protocol> > Found 1 initializing transitions I@16:54:34.943 spec-protocol> > Found 24 transitions I@16:54:34.952 spec-protocol> > No constant initializer I@16:54:34.952 spec-protocol> > Applying unique renaming I@16:54:34.952 spec-protocol> PASS #11: OptimizationPass I@16:54:34.968 spec-protocol> > Applying optimizations: I@16:54:34.969 spec-protocol> > ConstSimplifier I@16:54:34.969 spec-protocol> > ExprOptimizer I@16:54:35.030 spec-protocol> > SetMembershipSimplifier I@16:54:35.036 spec-protocol> > ConstSimplifier I@16:54:35.039 spec-protocol> PASS #12: AnalysisPass I@16:54:35.096 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:54:35.096 spec-protocol> > Skolemization I@16:54:35.096 spec-protocol> > Expansion I@16:54:35.099 spec-protocol> > Remove unused let-in defs I@16:54:35.108 spec-protocol> > Running analyzers... I@16:54:35.111 spec-protocol> > Introduced expression grades I@16:54:35.112 spec-protocol> PASS #13: BoundedChecker I@16:54:35.112 spec-protocol> State 0: Checking 5 state invariants I@16:54:35.657 spec-protocol> State 0: state invariant 0 holds. I@16:54:35.658 spec-protocol> State 0: state invariant 1 holds. I@16:54:35.659 spec-protocol> State 0: state invariant 2 holds. I@16:54:35.660 spec-protocol> State 0: state invariant 3 holds. I@16:54:35.665 spec-protocol> State 0: state invariant 4 holds. I@16:54:35.697 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:54:35.698 spec-protocol> The outcome is: NoError I@16:54:35.708 spec-protocol> [ok] No violation found (29526ms). 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