this derivation will be built: /nix/store/qyx20aqdzlz3m7crjklxpwl8098aw14p-spec-protocol.drv building '/nix/store/qyx20aqdzlz3m7crjklxpwl8098aw14p-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-11T16-54-36_5371467477638688027 spec-protocol> # APALACHE version: 0.56.1 | build: 70cdaf4 I@16:54:36.706 spec-protocol> Starting checker server on port 8822... I@16:54:36.715 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: 0e:83:08:69:b9:04:15:01 W@16:54:37.439 spec-protocol> Oct 11, 2026 4:54:40 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:40.678 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:54:41.400 spec-protocol> > Running Snowcat .::. I@16:54:41.401 spec-protocol> > Your types are purrfect! I@16:54:43.711 spec-protocol> > All expressions are typed I@16:54:43.711 spec-protocol> PASS #2: ConfigurationPass I@16:54:43.713 spec-protocol> > Set the initialization predicate to q::init I@16:54:43.717 spec-protocol> > Set the transition predicate to q::step I@16:54:43.717 spec-protocol> > Set an invariant to q::inductiveInv I@16:54:43.718 spec-protocol> PASS #3: DesugarerPass I@16:54:43.724 spec-protocol> > Desugaring... I@16:54:43.724 spec-protocol> PASS #4: InlinePass I@16:54:43.738 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:43.739 spec-protocol> PASS #5: TemporalPass I@16:54:43.836 spec-protocol> > Rewriting temporal operators... I@16:54:43.836 spec-protocol> > No temporal property specified, nothing to encode I@16:54:43.836 spec-protocol> PASS #6: InlinePass I@16:54:43.836 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:43.836 spec-protocol> PASS #7: PrimingPass I@16:54:43.860 spec-protocol> > Introducing q::initPrimed for q::init' I@16:54:43.862 spec-protocol> PASS #8: VCGen I@16:54:43.864 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@16:54:43.864 spec-protocol> > VCGen produced 39 verification condition(s) I@16:54:43.873 spec-protocol> PASS #9: PreprocessingPass I@16:54:43.876 spec-protocol> > Before preprocessing: unique renaming I@16:54:43.876 spec-protocol> > Applying standard transformations: I@16:54:43.882 spec-protocol> > PrimePropagation I@16:54:43.882 spec-protocol> > Desugarer I@16:54:43.889 spec-protocol> > UniqueRenamer I@16:54:43.898 spec-protocol> > Normalizer I@16:54:43.921 spec-protocol> > Keramelizer I@16:54:43.939 spec-protocol> > After preprocessing: UniqueRenamer I@16:54:43.966 spec-protocol> PASS #10: TransitionFinderPass I@16:54:44.006 spec-protocol> > Found 1 initializing transitions I@16:54:44.020 spec-protocol> > Found 24 transitions I@16:54:44.052 spec-protocol> > No constant initializer I@16:54:44.053 spec-protocol> > Applying unique renaming I@16:54:44.054 spec-protocol> PASS #11: OptimizationPass I@16:54:44.082 spec-protocol> > Applying optimizations: I@16:54:44.089 spec-protocol> > ConstSimplifier I@16:54:44.090 spec-protocol> > ExprOptimizer I@16:54:44.153 spec-protocol> > SetMembershipSimplifier I@16:54:44.180 spec-protocol> > ConstSimplifier I@16:54:44.187 spec-protocol> PASS #12: AnalysisPass I@16:54:44.247 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:54:44.249 spec-protocol> > Skolemization I@16:54:44.250 spec-protocol> > Expansion I@16:54:44.254 spec-protocol> > Remove unused let-in defs I@16:54:44.272 spec-protocol> > Running analyzers... I@16:54:44.284 spec-protocol> > Introduced expression grades I@16:54:44.292 spec-protocol> PASS #13: BoundedChecker I@16:54:44.292 spec-protocol> State 0: Checking 39 state invariants I@16:54:44.674 spec-protocol> State 0: state invariant 0 holds. I@16:54:44.677 spec-protocol> State 0: state invariant 1 holds. I@16:54:44.720 spec-protocol> State 0: state invariant 2 holds. I@16:54:44.722 spec-protocol> State 0: state invariant 3 holds. I@16:54:44.723 spec-protocol> State 0: state invariant 4 holds. I@16:54:44.747 spec-protocol> State 0: state invariant 5 holds. I@16:54:44.751 spec-protocol> State 0: state invariant 6 holds. I@16:54:44.752 spec-protocol> State 0: state invariant 7 holds. I@16:54:44.755 spec-protocol> State 0: state invariant 8 holds. I@16:54:44.757 spec-protocol> State 0: state invariant 9 holds. I@16:54:44.763 spec-protocol> State 0: state invariant 10 holds. I@16:54:44.764 spec-protocol> State 0: state invariant 11 holds. I@16:54:44.764 spec-protocol> State 0: state invariant 12 holds. I@16:54:44.773 spec-protocol> State 0: state invariant 13 holds. I@16:54:44.774 spec-protocol> State 0: state invariant 14 holds. I@16:54:44.780 spec-protocol> State 0: state invariant 15 holds. I@16:54:44.781 spec-protocol> State 0: state invariant 16 holds. I@16:54:44.782 spec-protocol> State 0: state invariant 17 holds. I@16:54:44.782 spec-protocol> State 0: state invariant 18 holds. I@16:54:44.785 spec-protocol> State 0: state invariant 19 holds. I@16:54:44.788 spec-protocol> State 0: state invariant 20 holds. I@16:54:44.793 spec-protocol> State 0: state invariant 21 holds. I@16:54:44.798 spec-protocol> State 0: state invariant 22 holds. I@16:54:44.801 spec-protocol> State 0: state invariant 23 holds. I@16:54:44.807 spec-protocol> State 0: state invariant 24 holds. I@16:54:44.809 spec-protocol> State 0: state invariant 25 holds. I@16:54:44.810 spec-protocol> State 0: state invariant 26 holds. I@16:54:44.814 spec-protocol> State 0: state invariant 27 holds. I@16:54:44.821 spec-protocol> State 0: state invariant 28 holds. I@16:54:44.835 spec-protocol> State 0: state invariant 29 holds. I@16:54:44.841 spec-protocol> State 0: state invariant 30 holds. I@16:54:44.859 spec-protocol> State 0: state invariant 31 holds. I@16:54:44.888 spec-protocol> State 0: state invariant 32 holds. I@16:54:44.914 spec-protocol> State 0: state invariant 33 holds. I@16:54:44.915 spec-protocol> State 0: state invariant 34 holds. I@16:54:44.918 spec-protocol> State 0: state invariant 35 holds. I@16:54:44.921 spec-protocol> State 0: state invariant 36 holds. I@16:54:44.922 spec-protocol> State 0: state invariant 37 holds. I@16:54:44.924 spec-protocol> State 0: state invariant 38 holds. I@16:54:44.924 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:54:44.924 spec-protocol> The outcome is: NoError I@16:54:44.933 spec-protocol> > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... spec-protocol> PASS #0: SanyParser I@16:54:45.337 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:54:45.500 spec-protocol> > Running Snowcat .::. I@16:54:45.500 spec-protocol> > Your types are purrfect! I@16:54:47.265 spec-protocol> > All expressions are typed I@16:54:47.266 spec-protocol> PASS #2: ConfigurationPass I@16:54:47.267 spec-protocol> > Set the initialization predicate to q::inductiveInv I@16:54:47.268 spec-protocol> > Set the transition predicate to q::step I@16:54:47.268 spec-protocol> > Set an invariant to q::inductiveInv I@16:54:47.268 spec-protocol> PASS #3: DesugarerPass I@16:54:47.270 spec-protocol> > Desugaring... I@16:54:47.270 spec-protocol> PASS #4: InlinePass I@16:54:47.272 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:47.272 spec-protocol> PASS #5: TemporalPass I@16:54:47.306 spec-protocol> > Rewriting temporal operators... I@16:54:47.306 spec-protocol> > No temporal property specified, nothing to encode I@16:54:47.306 spec-protocol> PASS #6: InlinePass I@16:54:47.306 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:47.306 spec-protocol> PASS #7: PrimingPass I@16:54:47.316 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:47.316 spec-protocol> PASS #8: VCGen I@16:54:47.318 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@16:54:47.318 spec-protocol> > VCGen produced 39 verification condition(s) I@16:54:47.319 spec-protocol> PASS #9: PreprocessingPass I@16:54:47.321 spec-protocol> > Before preprocessing: unique renaming I@16:54:47.321 spec-protocol> > Applying standard transformations: I@16:54:47.321 spec-protocol> > PrimePropagation I@16:54:47.321 spec-protocol> > Desugarer I@16:54:47.324 spec-protocol> > UniqueRenamer I@16:54:47.328 spec-protocol> > Normalizer I@16:54:47.339 spec-protocol> > Keramelizer I@16:54:47.354 spec-protocol> > After preprocessing: UniqueRenamer I@16:54:47.365 spec-protocol> PASS #10: TransitionFinderPass I@16:54:47.379 spec-protocol> > Found 1 initializing transitions I@16:54:47.381 spec-protocol> > Found 24 transitions I@16:54:47.391 spec-protocol> > No constant initializer I@16:54:47.392 spec-protocol> > Applying unique renaming I@16:54:47.392 spec-protocol> PASS #11: OptimizationPass I@16:54:47.413 spec-protocol> > Applying optimizations: I@16:54:47.413 spec-protocol> > ConstSimplifier I@16:54:47.413 spec-protocol> > ExprOptimizer I@16:54:47.487 spec-protocol> > SetMembershipSimplifier I@16:54:47.501 spec-protocol> > ConstSimplifier I@16:54:47.506 spec-protocol> PASS #12: AnalysisPass I@16:54:47.567 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:54:47.567 spec-protocol> > Skolemization I@16:54:47.567 spec-protocol> > Expansion I@16:54:47.571 spec-protocol> > Remove unused let-in defs I@16:54:47.583 spec-protocol> > Running analyzers... I@16:54:47.586 spec-protocol> > Introduced expression grades I@16:54:47.588 spec-protocol> PASS #13: BoundedChecker I@16:54:47.588 spec-protocol> State 0: Checking 39 state invariants I@16:54:48.241 spec-protocol> State 0: state invariant 0 holds. I@16:54:48.242 spec-protocol> State 0: state invariant 1 holds. I@16:54:48.266 spec-protocol> State 0: state invariant 2 holds. I@16:54:48.269 spec-protocol> State 0: state invariant 3 holds. I@16:54:48.270 spec-protocol> State 0: state invariant 4 holds. I@16:54:48.290 spec-protocol> State 0: state invariant 5 holds. I@16:54:48.299 spec-protocol> State 0: state invariant 6 holds. I@16:54:48.301 spec-protocol> State 0: state invariant 7 holds. I@16:54:48.302 spec-protocol> State 0: state invariant 8 holds. I@16:54:48.303 spec-protocol> State 0: state invariant 9 holds. I@16:54:48.304 spec-protocol> State 0: state invariant 10 holds. I@16:54:48.306 spec-protocol> State 0: state invariant 11 holds. I@16:54:48.307 spec-protocol> State 0: state invariant 12 holds. I@16:54:48.313 spec-protocol> State 0: state invariant 13 holds. I@16:54:48.314 spec-protocol> State 0: state invariant 14 holds. I@16:54:48.321 spec-protocol> State 0: state invariant 15 holds. I@16:54:48.322 spec-protocol> State 0: state invariant 16 holds. I@16:54:48.323 spec-protocol> State 0: state invariant 17 holds. I@16:54:48.324 spec-protocol> State 0: state invariant 18 holds. I@16:54:48.329 spec-protocol> State 0: state invariant 19 holds. I@16:54:48.334 spec-protocol> State 0: state invariant 20 holds. I@16:54:48.341 spec-protocol> State 0: state invariant 21 holds. I@16:54:48.353 spec-protocol> State 0: state invariant 22 holds. I@16:54:48.360 spec-protocol> State 0: state invariant 23 holds. I@16:54:48.367 spec-protocol> State 0: state invariant 24 holds. I@16:54:48.368 spec-protocol> State 0: state invariant 25 holds. I@16:54:48.368 spec-protocol> State 0: state invariant 26 holds. I@16:54:48.370 spec-protocol> State 0: state invariant 27 holds. I@16:54:48.374 spec-protocol> State 0: state invariant 28 holds. I@16:54:48.397 spec-protocol> State 0: state invariant 29 holds. I@16:54:48.403 spec-protocol> State 0: state invariant 30 holds. I@16:54:48.518 spec-protocol> State 0: state invariant 31 holds. I@16:54:48.645 spec-protocol> State 0: state invariant 32 holds. I@16:54:48.785 spec-protocol> State 0: state invariant 33 holds. I@16:54:48.789 spec-protocol> State 0: state invariant 34 holds. I@16:54:48.794 spec-protocol> State 0: state invariant 35 holds. I@16:54:48.798 spec-protocol> State 0: state invariant 36 holds. I@16:54:48.799 spec-protocol> State 0: state invariant 37 holds. I@16:54:48.800 spec-protocol> State 0: state invariant 38 holds. I@16:54:48.801 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:54:48.802 spec-protocol> State 1: Checking 12 state invariants I@16:54:48.829 spec-protocol> State 1: state invariant 0 holds. I@16:54:48.830 spec-protocol> State 1: state invariant 1 holds. I@16:54:48.853 spec-protocol> State 1: state invariant 18 holds. I@16:54:48.860 spec-protocol> State 1: state invariant 19 holds. I@16:54:48.865 spec-protocol> State 1: state invariant 20 holds. I@16:54:48.873 spec-protocol> State 1: state invariant 21 holds. I@16:54:48.881 spec-protocol> State 1: state invariant 27 holds. I@16:54:48.889 spec-protocol> State 1: state invariant 28 holds. I@16:54:48.914 spec-protocol> State 1: state invariant 29 holds. I@16:54:48.920 spec-protocol> State 1: state invariant 30 holds. I@16:54:49.043 spec-protocol> State 1: state invariant 31 holds. I@16:54:49.164 spec-protocol> State 1: state invariant 32 holds. I@16:54:49.255 spec-protocol> State 1: Checking 4 state invariants I@16:54:49.276 spec-protocol> State 1: state invariant 13 holds. I@16:54:49.278 spec-protocol> State 1: state invariant 29 holds. I@16:54:49.283 spec-protocol> State 1: state invariant 30 holds. I@16:54:49.395 spec-protocol> State 1: state invariant 31 holds. I@16:54:49.515 spec-protocol> State 1: Checking 16 state invariants I@16:54:49.562 spec-protocol> State 1: state invariant 0 holds. I@16:54:49.563 spec-protocol> State 1: state invariant 1 holds. I@16:54:49.583 spec-protocol> State 1: state invariant 3 holds. I@16:54:49.586 spec-protocol> State 1: state invariant 4 holds. I@16:54:49.604 spec-protocol> State 1: state invariant 5 holds. I@16:54:49.612 spec-protocol> State 1: state invariant 18 holds. I@16:54:49.618 spec-protocol> State 1: state invariant 19 holds. I@16:54:49.624 spec-protocol> State 1: state invariant 20 holds. I@16:54:49.631 spec-protocol> State 1: state invariant 21 holds. I@16:54:49.638 spec-protocol> State 1: state invariant 23 holds. I@16:54:49.647 spec-protocol> State 1: state invariant 27 holds. I@16:54:49.652 spec-protocol> State 1: state invariant 28 holds. I@16:54:49.670 spec-protocol> State 1: state invariant 29 holds. I@16:54:49.677 spec-protocol> State 1: state invariant 30 holds. I@16:54:49.767 spec-protocol> State 1: state invariant 31 holds. I@16:54:49.867 spec-protocol> State 1: state invariant 32 holds. I@16:54:49.947 spec-protocol> State 1: Checking 6 state invariants I@16:54:49.966 spec-protocol> State 1: state invariant 2 holds. I@16:54:49.967 spec-protocol> State 1: state invariant 27 holds. I@16:54:49.982 spec-protocol> State 1: state invariant 29 holds. I@16:54:49.987 spec-protocol> State 1: state invariant 30 holds. I@16:54:50.112 spec-protocol> State 1: state invariant 31 holds. I@16:54:50.234 spec-protocol> State 1: state invariant 38 holds. I@16:54:50.238 spec-protocol> State 1: Checking 15 state invariants I@16:54:50.256 spec-protocol> State 1: state invariant 0 holds. I@16:54:50.257 spec-protocol> State 1: state invariant 1 holds. I@16:54:50.286 spec-protocol> State 1: state invariant 2 holds. I@16:54:50.290 spec-protocol> State 1: state invariant 12 holds. I@16:54:50.300 spec-protocol> State 1: state invariant 18 holds. I@16:54:50.312 spec-protocol> State 1: state invariant 19 holds. I@16:54:50.321 spec-protocol> State 1: state invariant 20 holds. I@16:54:50.330 spec-protocol> State 1: state invariant 21 holds. I@16:54:50.340 spec-protocol> State 1: state invariant 27 holds. I@16:54:50.350 spec-protocol> State 1: state invariant 28 holds. I@16:54:50.381 spec-protocol> State 1: state invariant 29 holds. I@16:54:50.390 spec-protocol> State 1: state invariant 30 holds. I@16:54:50.530 spec-protocol> State 1: state invariant 31 holds. I@16:54:50.669 spec-protocol> State 1: state invariant 32 holds. I@16:54:50.827 spec-protocol> State 1: state invariant 37 holds. I@16:54:50.831 spec-protocol> State 1: Checking 18 state invariants I@16:54:51.104 spec-protocol> State 1: state invariant 9 holds. I@16:54:51.110 spec-protocol> State 1: state invariant 10 holds. I@16:54:51.113 spec-protocol> State 1: state invariant 11 holds. I@16:54:51.115 spec-protocol> State 1: state invariant 14 holds. I@16:54:51.147 spec-protocol> State 1: state invariant 15 holds. I@16:54:51.151 spec-protocol> State 1: state invariant 17 holds. I@16:54:51.153 spec-protocol> State 1: state invariant 22 holds. I@16:54:51.163 spec-protocol> State 1: state invariant 24 holds. I@16:54:51.166 spec-protocol> State 1: state invariant 26 holds. I@16:54:51.169 spec-protocol> State 1: state invariant 27 holds. I@16:54:51.179 spec-protocol> State 1: state invariant 28 holds. I@16:54:51.207 spec-protocol> State 1: state invariant 29 holds. I@16:54:51.216 spec-protocol> State 1: state invariant 30 holds. I@16:54:51.429 spec-protocol> State 1: state invariant 31 holds. I@16:54:51.507 spec-protocol> State 1: state invariant 32 holds. I@16:54:51.620 spec-protocol> State 1: state invariant 33 holds. I@16:54:51.625 spec-protocol> State 1: state invariant 34 holds. I@16:54:51.632 spec-protocol> State 1: state invariant 35 holds. I@16:54:51.647 spec-protocol> State 1: Checking 14 state invariants I@16:54:51.842 spec-protocol> State 1: state invariant 9 holds. I@16:54:51.846 spec-protocol> State 1: state invariant 10 holds. I@16:54:51.849 spec-protocol> State 1: state invariant 11 holds. I@16:54:51.851 spec-protocol> State 1: state invariant 14 holds. I@16:54:51.859 spec-protocol> State 1: state invariant 15 holds. I@16:54:51.863 spec-protocol> State 1: state invariant 17 holds. I@16:54:51.865 spec-protocol> State 1: state invariant 24 holds. I@16:54:51.867 spec-protocol> State 1: state invariant 26 holds. I@16:54:51.870 spec-protocol> State 1: state invariant 27 holds. I@16:54:51.876 spec-protocol> State 1: state invariant 28 holds. I@16:54:51.890 spec-protocol> State 1: state invariant 29 holds. I@16:54:51.897 spec-protocol> State 1: state invariant 30 holds. I@16:54:51.949 spec-protocol> State 1: state invariant 31 holds. I@16:54:52.017 spec-protocol> State 1: state invariant 32 holds. I@16:54:52.074 spec-protocol> State 1: Checking 26 state invariants I@16:54:52.186 spec-protocol> State 1: state invariant 0 holds. I@16:54:52.188 spec-protocol> State 1: state invariant 1 holds. I@16:54:52.213 spec-protocol> State 1: state invariant 9 holds. I@16:54:52.223 spec-protocol> State 1: state invariant 10 holds. I@16:54:52.226 spec-protocol> State 1: state invariant 11 holds. I@16:54:52.229 spec-protocol> State 1: state invariant 12 holds. I@16:54:52.235 spec-protocol> State 1: state invariant 14 holds. I@16:54:52.246 spec-protocol> State 1: state invariant 15 holds. I@16:54:52.253 spec-protocol> State 1: state invariant 17 holds. I@16:54:52.256 spec-protocol> State 1: state invariant 18 holds. I@16:54:52.265 spec-protocol> State 1: state invariant 19 holds. I@16:54:52.275 spec-protocol> State 1: state invariant 20 holds. I@16:54:52.289 spec-protocol> State 1: state invariant 21 holds. I@16:54:52.302 spec-protocol> State 1: state invariant 22 holds. I@16:54:52.312 spec-protocol> State 1: state invariant 23 holds. I@16:54:52.320 spec-protocol> State 1: state invariant 24 holds. I@16:54:52.322 spec-protocol> State 1: state invariant 26 holds. I@16:54:52.325 spec-protocol> State 1: state invariant 27 holds. I@16:54:52.345 spec-protocol> State 1: state invariant 28 holds. I@16:54:52.376 spec-protocol> State 1: state invariant 29 holds. I@16:54:52.384 spec-protocol> State 1: state invariant 30 holds. I@16:54:52.581 spec-protocol> State 1: state invariant 31 holds. I@16:54:52.746 spec-protocol> State 1: state invariant 32 holds. I@16:54:52.913 spec-protocol> State 1: state invariant 33 holds. I@16:54:52.919 spec-protocol> State 1: state invariant 34 holds. I@16:54:52.928 spec-protocol> State 1: state invariant 35 holds. I@16:54:52.941 spec-protocol> State 1: Checking 22 state invariants I@16:54:53.062 spec-protocol> State 1: state invariant 0 holds. I@16:54:53.063 spec-protocol> State 1: state invariant 1 holds. I@16:54:53.085 spec-protocol> State 1: state invariant 9 holds. I@16:54:53.097 spec-protocol> State 1: state invariant 10 holds. I@16:54:53.099 spec-protocol> State 1: state invariant 11 holds. I@16:54:53.101 spec-protocol> State 1: state invariant 12 holds. I@16:54:53.106 spec-protocol> State 1: state invariant 14 holds. I@16:54:53.117 spec-protocol> State 1: state invariant 15 holds. I@16:54:53.133 spec-protocol> State 1: state invariant 17 holds. I@16:54:53.135 spec-protocol> State 1: state invariant 18 holds. I@16:54:53.145 spec-protocol> State 1: state invariant 19 holds. I@16:54:53.164 spec-protocol> State 1: state invariant 20 holds. I@16:54:53.173 spec-protocol> State 1: state invariant 21 holds. I@16:54:53.187 spec-protocol> State 1: state invariant 23 holds. I@16:54:53.195 spec-protocol> State 1: state invariant 24 holds. I@16:54:53.197 spec-protocol> State 1: state invariant 26 holds. I@16:54:53.201 spec-protocol> State 1: state invariant 27 holds. I@16:54:53.229 spec-protocol> State 1: state invariant 28 holds. I@16:54:53.258 spec-protocol> State 1: state invariant 29 holds. I@16:54:53.265 spec-protocol> State 1: state invariant 30 holds. I@16:54:53.468 spec-protocol> State 1: state invariant 31 holds. I@16:54:53.625 spec-protocol> State 1: state invariant 32 holds. I@16:54:53.826 spec-protocol> Step 1: Transition #10 is disabled I@16:54:53.891 spec-protocol> Step 1: Transition #11 is disabled I@16:54:53.935 spec-protocol> State 1: Checking 27 state invariants I@16:54:54.099 spec-protocol> State 1: state invariant 0 holds. I@16:54:54.102 spec-protocol> State 1: state invariant 1 holds. I@16:54:54.134 spec-protocol> State 1: state invariant 9 holds. I@16:54:54.149 spec-protocol> State 1: state invariant 10 holds. I@16:54:54.152 spec-protocol> State 1: state invariant 12 holds. I@16:54:54.160 spec-protocol> State 1: state invariant 13 holds. I@16:54:54.163 spec-protocol> State 1: state invariant 14 holds. I@16:54:54.172 spec-protocol> State 1: state invariant 15 holds. I@16:54:54.189 spec-protocol> State 1: state invariant 16 holds. I@16:54:54.192 spec-protocol> State 1: state invariant 17 holds. I@16:54:54.194 spec-protocol> State 1: state invariant 18 holds. I@16:54:54.203 spec-protocol> State 1: state invariant 19 holds. I@16:54:54.217 spec-protocol> State 1: state invariant 20 holds. I@16:54:54.226 spec-protocol> State 1: state invariant 21 holds. I@16:54:54.240 spec-protocol> State 1: state invariant 22 holds. I@16:54:54.252 spec-protocol> State 1: state invariant 23 holds. I@16:54:54.262 spec-protocol> State 1: state invariant 24 holds. I@16:54:54.266 spec-protocol> State 1: state invariant 26 holds. I@16:54:54.271 spec-protocol> State 1: state invariant 27 holds. I@16:54:54.290 spec-protocol> State 1: state invariant 28 holds. I@16:54:54.330 spec-protocol> State 1: state invariant 29 holds. I@16:54:54.339 spec-protocol> State 1: state invariant 30 holds. I@16:54:54.475 spec-protocol> State 1: state invariant 31 holds. I@16:54:54.633 spec-protocol> State 1: state invariant 32 holds. I@16:54:54.772 spec-protocol> State 1: state invariant 33 holds. I@16:54:54.777 spec-protocol> State 1: state invariant 34 holds. I@16:54:54.784 spec-protocol> State 1: state invariant 35 holds. I@16:54:54.796 spec-protocol> State 1: Checking 23 state invariants I@16:54:54.947 spec-protocol> State 1: state invariant 0 holds. I@16:54:54.949 spec-protocol> State 1: state invariant 1 holds. I@16:54:54.980 spec-protocol> State 1: state invariant 9 holds. I@16:54:54.988 spec-protocol> State 1: state invariant 10 holds. I@16:54:54.991 spec-protocol> State 1: state invariant 12 holds. I@16:54:54.998 spec-protocol> State 1: state invariant 13 holds. I@16:54:55.000 spec-protocol> State 1: state invariant 14 holds. I@16:54:55.009 spec-protocol> State 1: state invariant 15 holds. I@16:54:55.017 spec-protocol> State 1: state invariant 16 holds. I@16:54:55.019 spec-protocol> State 1: state invariant 17 holds. I@16:54:55.021 spec-protocol> State 1: state invariant 18 holds. I@16:54:55.029 spec-protocol> State 1: state invariant 19 holds. I@16:54:55.041 spec-protocol> State 1: state invariant 20 holds. I@16:54:55.051 spec-protocol> State 1: state invariant 21 holds. I@16:54:55.062 spec-protocol> State 1: state invariant 23 holds. I@16:54:55.072 spec-protocol> State 1: state invariant 24 holds. I@16:54:55.074 spec-protocol> State 1: state invariant 26 holds. I@16:54:55.084 spec-protocol> State 1: state invariant 27 holds. I@16:54:55.093 spec-protocol> State 1: state invariant 28 holds. I@16:54:55.113 spec-protocol> State 1: state invariant 29 holds. I@16:54:55.122 spec-protocol> State 1: state invariant 30 holds. I@16:54:55.264 spec-protocol> State 1: state invariant 31 holds. I@16:54:55.426 spec-protocol> State 1: state invariant 32 holds. I@16:54:55.537 spec-protocol> State 1: Checking 26 state invariants I@16:54:55.895 spec-protocol> State 1: state invariant 0 holds. I@16:54:55.897 spec-protocol> State 1: state invariant 1 holds. I@16:54:55.927 spec-protocol> State 1: state invariant 9 holds. I@16:54:55.939 spec-protocol> State 1: state invariant 10 holds. I@16:54:55.942 spec-protocol> State 1: state invariant 12 holds. I@16:54:55.950 spec-protocol> State 1: state invariant 14 holds. I@16:54:55.959 spec-protocol> State 1: state invariant 15 holds. I@16:54:55.962 spec-protocol> State 1: state invariant 16 holds. I@16:54:55.964 spec-protocol> State 1: state invariant 17 holds. I@16:54:55.966 spec-protocol> State 1: state invariant 18 holds. I@16:54:55.975 spec-protocol> State 1: state invariant 19 holds. I@16:54:55.985 spec-protocol> State 1: state invariant 20 holds. I@16:54:55.995 spec-protocol> State 1: state invariant 21 holds. I@16:54:56.021 spec-protocol> State 1: state invariant 22 holds. I@16:54:56.043 spec-protocol> State 1: state invariant 23 holds. I@16:54:56.053 spec-protocol> State 1: state invariant 24 holds. I@16:54:56.056 spec-protocol> State 1: state invariant 26 holds. I@16:54:56.061 spec-protocol> State 1: state invariant 27 holds. I@16:54:56.074 spec-protocol> State 1: state invariant 28 holds. I@16:54:56.100 spec-protocol> State 1: state invariant 29 holds. I@16:54:56.108 spec-protocol> State 1: state invariant 30 holds. I@16:54:56.239 spec-protocol> State 1: state invariant 31 holds. I@16:54:56.382 spec-protocol> State 1: state invariant 32 holds. I@16:54:56.598 spec-protocol> State 1: state invariant 33 holds. I@16:54:56.605 spec-protocol> State 1: state invariant 34 holds. I@16:54:56.615 spec-protocol> State 1: state invariant 35 holds. I@16:54:56.645 spec-protocol> State 1: Checking 22 state invariants I@16:54:56.953 spec-protocol> State 1: state invariant 0 holds. I@16:54:56.955 spec-protocol> State 1: state invariant 1 holds. I@16:54:56.979 spec-protocol> State 1: state invariant 9 holds. I@16:54:56.987 spec-protocol> State 1: state invariant 10 holds. I@16:54:56.989 spec-protocol> State 1: state invariant 12 holds. I@16:54:56.995 spec-protocol> State 1: state invariant 14 holds. I@16:54:57.003 spec-protocol> State 1: state invariant 15 holds. I@16:54:57.018 spec-protocol> State 1: state invariant 16 holds. I@16:54:57.020 spec-protocol> State 1: state invariant 17 holds. I@16:54:57.022 spec-protocol> State 1: state invariant 18 holds. I@16:54:57.029 spec-protocol> State 1: state invariant 19 holds. I@16:54:57.040 spec-protocol> State 1: state invariant 20 holds. I@16:54:57.050 spec-protocol> State 1: state invariant 21 holds. I@16:54:57.063 spec-protocol> State 1: state invariant 23 holds. I@16:54:57.070 spec-protocol> State 1: state invariant 24 holds. I@16:54:57.073 spec-protocol> State 1: state invariant 26 holds. I@16:54:57.079 spec-protocol> State 1: state invariant 27 holds. I@16:54:57.094 spec-protocol> State 1: state invariant 28 holds. I@16:54:57.113 spec-protocol> State 1: state invariant 29 holds. I@16:54:57.120 spec-protocol> State 1: state invariant 30 holds. I@16:54:57.238 spec-protocol> State 1: state invariant 31 holds. I@16:54:57.623 spec-protocol> State 1: state invariant 32 holds. I@16:54:57.722 spec-protocol> Step 1: Transition #16 is disabled I@16:54:57.761 spec-protocol> State 1: Checking 21 state invariants I@16:54:57.851 spec-protocol> State 1: state invariant 0 holds. I@16:54:57.853 spec-protocol> State 1: state invariant 1 holds. I@16:54:57.876 spec-protocol> State 1: state invariant 9 holds. I@16:54:57.887 spec-protocol> State 1: state invariant 10 holds. I@16:54:57.889 spec-protocol> State 1: state invariant 12 holds. I@16:54:57.895 spec-protocol> State 1: state invariant 14 holds. I@16:54:57.903 spec-protocol> State 1: state invariant 15 holds. I@16:54:57.907 spec-protocol> State 1: state invariant 17 holds. I@16:54:57.909 spec-protocol> State 1: state invariant 18 holds. I@16:54:57.917 spec-protocol> State 1: state invariant 19 holds. I@16:54:57.925 spec-protocol> State 1: state invariant 20 holds. I@16:54:57.935 spec-protocol> State 1: state invariant 21 holds. I@16:54:57.951 spec-protocol> State 1: state invariant 23 holds. I@16:54:57.959 spec-protocol> State 1: state invariant 24 holds. I@16:54:57.961 spec-protocol> State 1: state invariant 26 holds. I@16:54:57.964 spec-protocol> State 1: state invariant 27 holds. I@16:54:57.974 spec-protocol> State 1: state invariant 28 holds. I@16:54:58.001 spec-protocol> State 1: state invariant 29 holds. I@16:54:58.008 spec-protocol> State 1: state invariant 30 holds. I@16:54:58.197 spec-protocol> State 1: state invariant 31 holds. I@16:54:58.358 spec-protocol> State 1: state invariant 32 holds. I@16:54:58.513 spec-protocol> Step 1: Transition #18 is disabled I@16:54:58.556 spec-protocol> State 1: Checking 21 state invariants I@16:54:58.618 spec-protocol> State 1: state invariant 0 holds. I@16:54:58.620 spec-protocol> State 1: state invariant 1 holds. I@16:54:58.646 spec-protocol> State 1: state invariant 9 holds. I@16:54:58.654 spec-protocol> State 1: state invariant 10 holds. I@16:54:58.656 spec-protocol> State 1: state invariant 12 holds. I@16:54:58.664 spec-protocol> State 1: state invariant 14 holds. I@16:54:58.671 spec-protocol> State 1: state invariant 15 holds. I@16:54:58.676 spec-protocol> State 1: state invariant 17 holds. I@16:54:58.678 spec-protocol> State 1: state invariant 18 holds. I@16:54:58.686 spec-protocol> State 1: state invariant 19 holds. I@16:54:58.699 spec-protocol> State 1: state invariant 20 holds. I@16:54:58.717 spec-protocol> State 1: state invariant 21 holds. I@16:54:58.732 spec-protocol> State 1: state invariant 23 holds. I@16:54:58.741 spec-protocol> State 1: state invariant 24 holds. I@16:54:58.743 spec-protocol> State 1: state invariant 26 holds. I@16:54:58.746 spec-protocol> State 1: state invariant 27 holds. I@16:54:58.773 spec-protocol> State 1: state invariant 28 holds. I@16:54:58.821 spec-protocol> State 1: state invariant 29 holds. I@16:54:58.829 spec-protocol> State 1: state invariant 30 holds. I@16:54:59.023 spec-protocol> State 1: state invariant 31 holds. I@16:54:59.223 spec-protocol> State 1: state invariant 32 holds. I@16:54:59.388 spec-protocol> Step 1: Transition #20 is disabled I@16:54:59.424 spec-protocol> Step 1: Transition #21 is disabled I@16:54:59.477 spec-protocol> State 1: Checking 14 state invariants I@16:54:59.549 spec-protocol> State 1: state invariant 6 holds. I@16:54:59.550 spec-protocol> State 1: state invariant 7 holds. I@16:54:59.552 spec-protocol> State 1: state invariant 22 holds. I@16:54:59.566 spec-protocol> State 1: state invariant 25 holds. I@16:54:59.580 spec-protocol> State 1: state invariant 27 holds. I@16:54:59.628 spec-protocol> State 1: state invariant 28 holds. I@16:54:59.687 spec-protocol> State 1: state invariant 29 holds. I@16:54:59.694 spec-protocol> State 1: state invariant 30 holds. I@16:54:59.828 spec-protocol> State 1: state invariant 31 holds. I@16:54:59.907 spec-protocol> State 1: state invariant 32 holds. I@16:54:59.995 spec-protocol> State 1: state invariant 33 holds. I@16:55:00.000 spec-protocol> State 1: state invariant 34 holds. I@16:55:00.006 spec-protocol> State 1: state invariant 35 holds. I@16:55:00.011 spec-protocol> State 1: state invariant 38 holds. I@16:55:00.013 spec-protocol> State 1: Checking 17 state invariants I@16:55:00.101 spec-protocol> State 1: state invariant 3 holds. I@16:55:00.103 spec-protocol> State 1: state invariant 4 holds. I@16:55:00.133 spec-protocol> State 1: state invariant 5 holds. I@16:55:00.147 spec-protocol> State 1: state invariant 6 holds. I@16:55:00.148 spec-protocol> State 1: state invariant 7 holds. I@16:55:00.149 spec-protocol> State 1: state invariant 22 holds. I@16:55:00.165 spec-protocol> State 1: state invariant 25 holds. I@16:55:00.167 spec-protocol> State 1: state invariant 27 holds. I@16:55:00.171 spec-protocol> State 1: state invariant 28 holds. I@16:55:00.214 spec-protocol> State 1: state invariant 29 holds. I@16:55:00.220 spec-protocol> State 1: state invariant 30 holds. I@16:55:00.451 spec-protocol> State 1: state invariant 31 holds. I@16:55:00.651 spec-protocol> State 1: state invariant 32 holds. I@16:55:00.865 spec-protocol> State 1: state invariant 33 holds. I@16:55:00.884 spec-protocol> State 1: state invariant 34 holds. I@16:55:00.890 spec-protocol> State 1: state invariant 35 holds. I@16:55:00.895 spec-protocol> State 1: state invariant 38 holds. I@16:55:00.897 spec-protocol> Step 1: picking a transition out of 17 transition(s) I@16:55:00.899 spec-protocol> The outcome is: NoError I@16:55:01.067 spec-protocol> > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... spec-protocol> PASS #0: SanyParser I@16:55:01.328 spec-protocol> PASS #1: TypeCheckerSnowcat I@16:55:01.422 spec-protocol> > Running Snowcat .::. I@16:55:01.422 spec-protocol> > Your types are purrfect! I@16:55:03.260 spec-protocol> > All expressions are typed I@16:55:03.261 spec-protocol> PASS #2: ConfigurationPass I@16:55:03.261 spec-protocol> > Set the initialization predicate to q::inductiveInv I@16:55:03.262 spec-protocol> > Set the transition predicate to q::step I@16:55:03.262 spec-protocol> > Set an invariant to q::inv I@16:55:03.262 spec-protocol> PASS #3: DesugarerPass I@16:55:03.264 spec-protocol> > Desugaring... I@16:55:03.264 spec-protocol> PASS #4: InlinePass I@16:55:03.265 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:55:03.265 spec-protocol> PASS #5: TemporalPass I@16:55:03.294 spec-protocol> > Rewriting temporal operators... I@16:55:03.294 spec-protocol> > No temporal property specified, nothing to encode I@16:55:03.294 spec-protocol> PASS #6: InlinePass I@16:55:03.294 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:55:03.294 spec-protocol> PASS #7: PrimingPass I@16:55:03.306 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:55:03.306 spec-protocol> PASS #8: VCGen I@16:55:03.307 spec-protocol> > Producing verification conditions from the invariant q::inv I@16:55:03.307 spec-protocol> > VCGen produced 5 verification condition(s) I@16:55:03.307 spec-protocol> PASS #9: PreprocessingPass I@16:55:03.307 spec-protocol> > Before preprocessing: unique renaming I@16:55:03.308 spec-protocol> > Applying standard transformations: I@16:55:03.308 spec-protocol> > PrimePropagation I@16:55:03.308 spec-protocol> > Desugarer I@16:55:03.313 spec-protocol> > UniqueRenamer I@16:55:03.316 spec-protocol> > Normalizer I@16:55:03.326 spec-protocol> > Keramelizer I@16:55:03.331 spec-protocol> > After preprocessing: UniqueRenamer I@16:55:03.339 spec-protocol> PASS #10: TransitionFinderPass I@16:55:03.352 spec-protocol> > Found 1 initializing transitions I@16:55:03.354 spec-protocol> > Found 24 transitions I@16:55:03.363 spec-protocol> > No constant initializer I@16:55:03.363 spec-protocol> > Applying unique renaming I@16:55:03.363 spec-protocol> PASS #11: OptimizationPass I@16:55:03.380 spec-protocol> > Applying optimizations: I@16:55:03.380 spec-protocol> > ConstSimplifier I@16:55:03.380 spec-protocol> > ExprOptimizer I@16:55:03.436 spec-protocol> > SetMembershipSimplifier I@16:55:03.444 spec-protocol> > ConstSimplifier I@16:55:03.448 spec-protocol> PASS #12: AnalysisPass I@16:55:03.499 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@16:55:03.499 spec-protocol> > Skolemization I@16:55:03.499 spec-protocol> > Expansion I@16:55:03.502 spec-protocol> > Remove unused let-in defs I@16:55:03.515 spec-protocol> > Running analyzers... I@16:55:03.518 spec-protocol> > Introduced expression grades I@16:55:03.519 spec-protocol> PASS #13: BoundedChecker I@16:55:03.519 spec-protocol> State 0: Checking 5 state invariants I@16:55:03.979 spec-protocol> State 0: state invariant 0 holds. I@16:55:03.980 spec-protocol> State 0: state invariant 1 holds. I@16:55:03.982 spec-protocol> State 0: state invariant 2 holds. I@16:55:03.983 spec-protocol> State 0: state invariant 3 holds. I@16:55:03.987 spec-protocol> State 0: state invariant 4 holds. I@16:55:04.016 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@16:55:04.018 spec-protocol> The outcome is: NoError I@16:55:04.033 spec-protocol> [ok] No violation found (28184ms). 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