this derivation will be built: /nix/store/dya24l1lmm138d3b1826q2h2fhp5vrh2-spec-protocol.drv these 4 paths will be fetched (568.0 MiB download, 852.7 MiB unpacked): /nix/store/ij5q131fzyqw8wh76y9nrj5jl45zviqw-openjdk-21.0.12+8 /nix/store/s90yin0j1q75gr8iyr11qxqzbjdssv25-quint-0.32.0 /nix/store/mx71fx62163cbid5nc6k7vvcmpg8r609-quint-cli-0.32.0 /nix/store/ma9wr3rh0rr0plzz5dmh87dxk734n7hk-set-java-classpath-hook warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy warning: unable to download 'https://hetzner-cache.numtide.com/nar/0gp3mbvcvz0rjqh9gnippmj29s473lbgsw9v7kwz158ka3ymmclz.nar.zst': HTTP error 200 (curl error: Stream error in the HTTP/2 framing layer); retrying from offset 20971520 in 84 ms (attempt 1/5) 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-08-30T17-05-40_12925069696982756512 spec-protocol> # APALACHE version: 0.56.1 | build: 70cdaf4 I@17:05:41.756 spec-protocol> Starting checker server on port 8822... I@17:05:41.793 spec-protocol> The Apalache server is running on port 8822. Press Ctrl-C to stop. spec-protocol> Failed to find a usable hardware address from the network interfaces; using random bytes: b9:d4:30:9b:30:13:b4:ce W@17:05:46.140 spec-protocol> Aug 30, 2026 5:05:54 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@17:05:58.250 spec-protocol> PASS #1: TypeCheckerSnowcat I@17:06:02.639 spec-protocol> > Running Snowcat .::. I@17:06:02.639 spec-protocol> > Your types are purrfect! I@17:06:14.109 spec-protocol> > All expressions are typed I@17:06:14.110 spec-protocol> PASS #2: ConfigurationPass I@17:06:14.112 spec-protocol> > Set the initialization predicate to q::init I@17:06:14.120 spec-protocol> > Set the transition predicate to q::step I@17:06:14.122 spec-protocol> > Set an invariant to q::inductiveInv I@17:06:14.124 spec-protocol> PASS #3: DesugarerPass I@17:06:14.135 spec-protocol> > Desugaring... I@17:06:14.138 spec-protocol> PASS #4: InlinePass I@17:06:14.168 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@17:06:14.170 spec-protocol> PASS #5: TemporalPass I@17:06:14.806 spec-protocol> > Rewriting temporal operators... I@17:06:14.819 spec-protocol> > No temporal property specified, nothing to encode I@17:06:14.823 spec-protocol> PASS #6: InlinePass I@17:06:15.049 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@17:06:15.055 spec-protocol> PASS #7: PrimingPass I@17:06:15.213 spec-protocol> > Introducing q::initPrimed for q::init' I@17:06:15.228 spec-protocol> PASS #8: VCGen I@17:06:15.243 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@17:06:15.245 spec-protocol> > VCGen produced 39 verification condition(s) I@17:06:15.299 spec-protocol> PASS #9: PreprocessingPass I@17:06:15.329 spec-protocol> > Before preprocessing: unique renaming I@17:06:15.329 spec-protocol> > Applying standard transformations: I@17:06:15.508 spec-protocol> > PrimePropagation I@17:06:15.514 spec-protocol> > Desugarer I@17:06:15.715 spec-protocol> > UniqueRenamer I@17:06:15.853 spec-protocol> > Normalizer I@17:06:16.150 spec-protocol> > Keramelizer I@17:06:16.259 spec-protocol> > After preprocessing: UniqueRenamer I@17:06:16.826 spec-protocol> PASS #10: TransitionFinderPass I@17:06:17.199 spec-protocol> > Found 1 initializing transitions I@17:06:17.224 spec-protocol> > Found 24 transitions I@17:06:17.435 spec-protocol> > No constant initializer I@17:06:17.437 spec-protocol> > Applying unique renaming I@17:06:17.439 spec-protocol> PASS #11: OptimizationPass I@17:06:17.527 spec-protocol> > Applying optimizations: I@17:06:17.548 spec-protocol> > ConstSimplifier I@17:06:17.550 spec-protocol> > ExprOptimizer I@17:06:17.940 spec-protocol> > SetMembershipSimplifier I@17:06:18.146 spec-protocol> > ConstSimplifier I@17:06:18.179 spec-protocol> PASS #12: AnalysisPass I@17:06:18.334 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@17:06:18.337 spec-protocol> > Skolemization I@17:06:18.338 spec-protocol> > Expansion I@17:06:18.377 spec-protocol> > Remove unused let-in defs I@17:06:18.484 spec-protocol> > Running analyzers... I@17:06:18.710 spec-protocol> > Introduced expression grades I@17:06:18.806 spec-protocol> PASS #13: BoundedChecker I@17:06:18.809 spec-protocol> State 0: Checking 39 state invariants I@17:06:22.295 spec-protocol> State 0: state invariant 0 holds. I@17:06:22.299 spec-protocol> State 0: state invariant 1 holds. I@17:06:22.411 spec-protocol> State 0: state invariant 2 holds. I@17:06:22.415 spec-protocol> State 0: state invariant 3 holds. I@17:06:22.423 spec-protocol> State 0: state invariant 4 holds. I@17:06:22.493 spec-protocol> State 0: state invariant 5 holds. I@17:06:22.506 spec-protocol> State 0: state invariant 6 holds. I@17:06:22.511 spec-protocol> State 0: state invariant 7 holds. I@17:06:22.515 spec-protocol> State 0: state invariant 8 holds. I@17:06:22.520 spec-protocol> State 0: state invariant 9 holds. I@17:06:22.550 spec-protocol> State 0: state invariant 10 holds. I@17:06:22.555 spec-protocol> State 0: state invariant 11 holds. I@17:06:22.557 spec-protocol> State 0: state invariant 12 holds. I@17:06:22.583 spec-protocol> State 0: state invariant 13 holds. I@17:06:22.587 spec-protocol> State 0: state invariant 14 holds. I@17:06:22.605 spec-protocol> State 0: state invariant 15 holds. I@17:06:22.609 spec-protocol> State 0: state invariant 16 holds. I@17:06:22.611 spec-protocol> State 0: state invariant 17 holds. I@17:06:22.616 spec-protocol> State 0: state invariant 18 holds. I@17:06:22.624 spec-protocol> State 0: state invariant 19 holds. I@17:06:22.633 spec-protocol> State 0: state invariant 20 holds. I@17:06:22.645 spec-protocol> State 0: state invariant 21 holds. I@17:06:22.657 spec-protocol> State 0: state invariant 22 holds. I@17:06:22.666 spec-protocol> State 0: state invariant 23 holds. I@17:06:22.680 spec-protocol> State 0: state invariant 24 holds. I@17:06:22.690 spec-protocol> State 0: state invariant 25 holds. I@17:06:22.695 spec-protocol> State 0: state invariant 26 holds. I@17:06:22.708 spec-protocol> State 0: state invariant 27 holds. I@17:06:22.732 spec-protocol> State 0: state invariant 28 holds. I@17:06:22.980 spec-protocol> State 0: state invariant 29 holds. I@17:06:22.997 spec-protocol> State 0: state invariant 30 holds. I@17:06:23.038 spec-protocol> State 0: state invariant 31 holds. I@17:06:23.168 spec-protocol> State 0: state invariant 32 holds. I@17:06:23.264 spec-protocol> State 0: state invariant 33 holds. I@17:06:23.271 spec-protocol> State 0: state invariant 34 holds. I@17:06:23.287 spec-protocol> State 0: state invariant 35 holds. I@17:06:23.304 spec-protocol> State 0: state invariant 36 holds. I@17:06:23.311 spec-protocol> State 0: state invariant 37 holds. I@17:06:23.319 spec-protocol> State 0: state invariant 38 holds. I@17:06:23.323 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@17:06:23.326 spec-protocol> The outcome is: NoError I@17:06:23.347 spec-protocol> > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... spec-protocol> PASS #0: SanyParser I@17:06:24.621 spec-protocol> PASS #1: TypeCheckerSnowcat I@17:06:25.045 spec-protocol> > Running Snowcat .::. I@17:06:25.046 spec-protocol> > Your types are purrfect! I@17:06:30.612 spec-protocol> > All expressions are typed I@17:06:30.613 spec-protocol> PASS #2: ConfigurationPass I@17:06:30.615 spec-protocol> > Set the initialization predicate to q::inductiveInv I@17:06:30.622 spec-protocol> > Set the transition predicate to q::step I@17:06:30.624 spec-protocol> > Set an invariant to q::inductiveInv I@17:06:30.625 spec-protocol> PASS #3: DesugarerPass I@17:06:30.638 spec-protocol> > Desugaring... I@17:06:30.639 spec-protocol> PASS #4: InlinePass I@17:06:30.646 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@17:06:30.648 spec-protocol> PASS #5: TemporalPass I@17:06:30.745 spec-protocol> > Rewriting temporal operators... I@17:06:30.746 spec-protocol> > No temporal property specified, nothing to encode I@17:06:30.747 spec-protocol> PASS #6: InlinePass I@17:06:30.750 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@17:06:30.754 spec-protocol> PASS #7: PrimingPass I@17:06:30.836 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@17:06:30.837 spec-protocol> PASS #8: VCGen I@17:06:30.846 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@17:06:30.847 spec-protocol> > VCGen produced 39 verification condition(s) I@17:06:30.853 spec-protocol> PASS #9: PreprocessingPass I@17:06:30.870 spec-protocol> > Before preprocessing: unique renaming I@17:06:30.870 spec-protocol> > Applying standard transformations: I@17:06:30.871 spec-protocol> > PrimePropagation I@17:06:30.871 spec-protocol> > Desugarer I@17:06:30.888 spec-protocol> > UniqueRenamer I@17:06:30.953 spec-protocol> > Normalizer I@17:06:31.071 spec-protocol> > Keramelizer I@17:06:31.128 spec-protocol> > After preprocessing: UniqueRenamer I@17:06:31.200 spec-protocol> PASS #10: TransitionFinderPass I@17:06:31.290 spec-protocol> > Found 1 initializing transitions I@17:06:31.297 spec-protocol> > Found 24 transitions I@17:06:31.328 spec-protocol> > No constant initializer I@17:06:31.328 spec-protocol> > Applying unique renaming I@17:06:31.331 spec-protocol> PASS #11: OptimizationPass I@17:06:31.857 spec-protocol> > Applying optimizations: I@17:06:31.857 spec-protocol> > ConstSimplifier I@17:06:31.858 spec-protocol> > ExprOptimizer I@17:06:31.994 spec-protocol> > SetMembershipSimplifier I@17:06:32.045 spec-protocol> > ConstSimplifier I@17:06:32.057 spec-protocol> PASS #12: AnalysisPass I@17:06:32.174 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@17:06:32.174 spec-protocol> > Skolemization I@17:06:32.175 spec-protocol> > Expansion I@17:06:32.187 spec-protocol> > Remove unused let-in defs I@17:06:32.278 spec-protocol> > Running analyzers... I@17:06:32.357 spec-protocol> > Introduced expression grades I@17:06:32.536 spec-protocol> PASS #13: BoundedChecker I@17:06:32.541 spec-protocol> State 0: Checking 39 state invariants I@17:06:36.872 spec-protocol> State 0: state invariant 0 holds. I@17:06:36.873 spec-protocol> State 0: state invariant 1 holds. I@17:06:36.924 spec-protocol> State 0: state invariant 2 holds. I@17:06:36.932 spec-protocol> State 0: state invariant 3 holds. I@17:06:36.936 spec-protocol> State 0: state invariant 4 holds. I@17:06:36.970 spec-protocol> State 0: state invariant 5 holds. I@17:06:36.987 spec-protocol> State 0: state invariant 6 holds. I@17:06:36.990 spec-protocol> State 0: state invariant 7 holds. I@17:06:36.992 spec-protocol> State 0: state invariant 8 holds. I@17:06:36.995 spec-protocol> State 0: state invariant 9 holds. I@17:06:36.997 spec-protocol> State 0: state invariant 10 holds. I@17:06:37.001 spec-protocol> State 0: state invariant 11 holds. I@17:06:37.003 spec-protocol> State 0: state invariant 12 holds. I@17:06:37.016 spec-protocol> State 0: state invariant 13 holds. I@17:06:37.020 spec-protocol> State 0: state invariant 14 holds. I@17:06:37.033 spec-protocol> State 0: state invariant 15 holds. I@17:06:37.036 spec-protocol> State 0: state invariant 16 holds. I@17:06:37.038 spec-protocol> State 0: state invariant 17 holds. I@17:06:37.040 spec-protocol> State 0: state invariant 18 holds. I@17:06:37.052 spec-protocol> State 0: state invariant 19 holds. I@17:06:37.067 spec-protocol> State 0: state invariant 20 holds. I@17:06:37.087 spec-protocol> State 0: state invariant 21 holds. I@17:06:37.124 spec-protocol> State 0: state invariant 22 holds. I@17:06:37.139 spec-protocol> State 0: state invariant 23 holds. I@17:06:37.160 spec-protocol> State 0: state invariant 24 holds. I@17:06:37.165 spec-protocol> State 0: state invariant 25 holds. I@17:06:37.169 spec-protocol> State 0: state invariant 26 holds. I@17:06:37.177 spec-protocol> State 0: state invariant 27 holds. I@17:06:37.195 spec-protocol> State 0: state invariant 28 holds. I@17:06:37.279 spec-protocol> State 0: state invariant 29 holds. I@17:06:37.293 spec-protocol> State 0: state invariant 30 holds. I@17:06:37.713 spec-protocol> State 0: state invariant 31 holds. I@17:06:38.130 spec-protocol> State 0: state invariant 32 holds. I@17:06:38.639 spec-protocol> State 0: state invariant 33 holds. I@17:06:38.652 spec-protocol> State 0: state invariant 34 holds. I@17:06:38.677 spec-protocol> State 0: state invariant 35 holds. I@17:06:38.686 spec-protocol> State 0: state invariant 36 holds. I@17:06:38.689 spec-protocol> State 0: state invariant 37 holds. I@17:06:38.691 spec-protocol> State 0: state invariant 38 holds. I@17:06:38.693 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@17:06:38.694 spec-protocol> State 1: Checking 12 state invariants I@17:06:38.736 spec-protocol> State 1: state invariant 0 holds. I@17:06:38.738 spec-protocol> State 1: state invariant 1 holds. I@17:06:38.774 spec-protocol> State 1: state invariant 18 holds. I@17:06:38.788 spec-protocol> State 1: state invariant 19 holds. I@17:06:38.798 spec-protocol> State 1: state invariant 20 holds. I@17:06:38.814 spec-protocol> State 1: state invariant 21 holds. I@17:06:38.833 spec-protocol> State 1: state invariant 27 holds. I@17:06:38.850 spec-protocol> State 1: state invariant 28 holds. I@17:06:38.909 spec-protocol> State 1: state invariant 29 holds. I@17:06:38.922 spec-protocol> State 1: state invariant 30 holds. I@17:06:39.224 spec-protocol> State 1: state invariant 31 holds. I@17:06:39.474 spec-protocol> State 1: state invariant 32 holds. I@17:06:39.657 spec-protocol> State 1: Checking 4 state invariants I@17:06:39.703 spec-protocol> State 1: state invariant 13 holds. I@17:06:39.709 spec-protocol> State 1: state invariant 29 holds. I@17:06:39.723 spec-protocol> State 1: state invariant 30 holds. I@17:06:39.958 spec-protocol> State 1: state invariant 31 holds. I@17:06:40.196 spec-protocol> State 1: Checking 16 state invariants I@17:06:40.345 spec-protocol> State 1: state invariant 0 holds. I@17:06:40.348 spec-protocol> State 1: state invariant 1 holds. I@17:06:40.406 spec-protocol> State 1: state invariant 3 holds. I@17:06:40.418 spec-protocol> State 1: state invariant 4 holds. I@17:06:40.458 spec-protocol> State 1: state invariant 5 holds. I@17:06:40.476 spec-protocol> State 1: state invariant 18 holds. I@17:06:40.496 spec-protocol> State 1: state invariant 19 holds. I@17:06:40.521 spec-protocol> State 1: state invariant 20 holds. I@17:06:40.540 spec-protocol> State 1: state invariant 21 holds. I@17:06:40.559 spec-protocol> State 1: state invariant 23 holds. I@17:06:40.580 spec-protocol> State 1: state invariant 27 holds. I@17:06:40.589 spec-protocol> State 1: state invariant 28 holds. I@17:06:40.623 spec-protocol> State 1: state invariant 29 holds. I@17:06:40.634 spec-protocol> State 1: state invariant 30 holds. I@17:06:40.915 spec-protocol> State 1: state invariant 31 holds. I@17:06:41.085 spec-protocol> State 1: state invariant 32 holds. I@17:06:41.221 spec-protocol> State 1: Checking 6 state invariants I@17:06:41.257 spec-protocol> State 1: state invariant 2 holds. I@17:06:41.259 spec-protocol> State 1: state invariant 27 holds. I@17:06:41.283 spec-protocol> State 1: state invariant 29 holds. I@17:06:41.293 spec-protocol> State 1: state invariant 30 holds. I@17:06:41.553 spec-protocol> State 1: state invariant 31 holds. I@17:06:41.785 spec-protocol> State 1: state invariant 38 holds. I@17:06:41.790 spec-protocol> State 1: Checking 15 state invariants I@17:06:41.813 spec-protocol> State 1: state invariant 0 holds. I@17:06:41.814 spec-protocol> State 1: state invariant 1 holds. I@17:06:41.857 spec-protocol> State 1: state invariant 2 holds. I@17:06:41.861 spec-protocol> State 1: state invariant 12 holds. I@17:06:41.875 spec-protocol> State 1: state invariant 18 holds. I@17:06:41.894 spec-protocol> State 1: state invariant 19 holds. I@17:06:41.909 spec-protocol> State 1: state invariant 20 holds. I@17:06:41.924 spec-protocol> State 1: state invariant 21 holds. I@17:06:41.942 spec-protocol> State 1: state invariant 27 holds. I@17:06:41.959 spec-protocol> State 1: state invariant 28 holds. I@17:06:42.018 spec-protocol> State 1: state invariant 29 holds. I@17:06:42.030 spec-protocol> State 1: state invariant 30 holds. I@17:06:42.336 spec-protocol> State 1: state invariant 31 holds. I@17:06:42.534 spec-protocol> State 1: state invariant 32 holds. I@17:06:42.786 spec-protocol> State 1: state invariant 37 holds. I@17:06:42.792 spec-protocol> State 1: Checking 18 state invariants I@17:06:43.151 spec-protocol> State 1: state invariant 9 holds. I@17:06:43.157 spec-protocol> State 1: state invariant 10 holds. I@17:06:43.165 spec-protocol> State 1: state invariant 11 holds. I@17:06:43.168 spec-protocol> State 1: state invariant 14 holds. I@17:06:43.226 spec-protocol> State 1: state invariant 15 holds. I@17:06:43.234 spec-protocol> State 1: state invariant 17 holds. I@17:06:43.238 spec-protocol> State 1: state invariant 22 holds. I@17:06:43.252 spec-protocol> State 1: state invariant 24 holds. I@17:06:43.256 spec-protocol> State 1: state invariant 26 holds. I@17:06:43.262 spec-protocol> State 1: state invariant 27 holds. I@17:06:43.277 spec-protocol> State 1: state invariant 28 holds. I@17:06:43.309 spec-protocol> State 1: state invariant 29 holds. I@17:06:43.324 spec-protocol> State 1: state invariant 30 holds. I@17:06:43.475 spec-protocol> State 1: state invariant 31 holds. I@17:06:43.597 spec-protocol> State 1: state invariant 32 holds. I@17:06:43.761 spec-protocol> State 1: state invariant 33 holds. I@17:06:43.770 spec-protocol> State 1: state invariant 34 holds. I@17:06:43.780 spec-protocol> State 1: state invariant 35 holds. I@17:06:43.803 spec-protocol> State 1: Checking 14 state invariants I@17:06:44.133 spec-protocol> State 1: state invariant 9 holds. I@17:06:44.139 spec-protocol> State 1: state invariant 10 holds. I@17:06:44.143 spec-protocol> State 1: state invariant 11 holds. I@17:06:44.145 spec-protocol> State 1: state invariant 14 holds. I@17:06:44.157 spec-protocol> State 1: state invariant 15 holds. I@17:06:44.164 spec-protocol> State 1: state invariant 17 holds. I@17:06:44.168 spec-protocol> State 1: state invariant 24 holds. I@17:06:44.171 spec-protocol> State 1: state invariant 26 holds. I@17:06:44.176 spec-protocol> State 1: state invariant 27 holds. I@17:06:44.186 spec-protocol> State 1: state invariant 28 holds. I@17:06:44.217 spec-protocol> State 1: state invariant 29 holds. I@17:06:44.229 spec-protocol> State 1: state invariant 30 holds. I@17:06:44.310 spec-protocol> State 1: state invariant 31 holds. I@17:06:44.416 spec-protocol> State 1: state invariant 32 holds. I@17:06:44.506 spec-protocol> State 1: Checking 26 state invariants I@17:06:44.696 spec-protocol> State 1: state invariant 0 holds. I@17:06:44.700 spec-protocol> State 1: state invariant 1 holds. I@17:06:44.745 spec-protocol> State 1: state invariant 9 holds. I@17:06:44.766 spec-protocol> State 1: state invariant 10 holds. I@17:06:44.776 spec-protocol> State 1: state invariant 11 holds. I@17:06:44.783 spec-protocol> State 1: state invariant 12 holds. I@17:06:44.795 spec-protocol> State 1: state invariant 14 holds. I@17:06:44.814 spec-protocol> State 1: state invariant 15 holds. I@17:06:44.834 spec-protocol> State 1: state invariant 17 holds. I@17:06:44.841 spec-protocol> State 1: state invariant 18 holds. I@17:06:44.856 spec-protocol> State 1: state invariant 19 holds. I@17:06:44.934 spec-protocol> State 1: state invariant 20 holds. I@17:06:44.954 spec-protocol> State 1: state invariant 21 holds. I@17:06:44.991 spec-protocol> State 1: state invariant 22 holds. I@17:06:45.042 spec-protocol> State 1: state invariant 23 holds. I@17:06:45.057 spec-protocol> State 1: state invariant 24 holds. I@17:06:45.064 spec-protocol> State 1: state invariant 26 holds. I@17:06:45.079 spec-protocol> State 1: state invariant 27 holds. I@17:06:45.130 spec-protocol> State 1: state invariant 28 holds. I@17:06:45.438 spec-protocol> State 1: state invariant 29 holds. I@17:06:45.470 spec-protocol> State 1: state invariant 30 holds. I@17:06:46.167 spec-protocol> State 1: state invariant 31 holds. I@17:06:46.630 spec-protocol> State 1: state invariant 32 holds. I@17:06:47.125 spec-protocol> State 1: state invariant 33 holds. I@17:06:47.141 spec-protocol> State 1: state invariant 34 holds. I@17:06:47.168 spec-protocol> State 1: state invariant 35 holds. I@17:06:47.212 spec-protocol> State 1: Checking 22 state invariants I@17:06:47.857 spec-protocol> State 1: state invariant 0 holds. I@17:06:47.863 spec-protocol> State 1: state invariant 1 holds. I@17:06:47.937 spec-protocol> State 1: state invariant 9 holds. I@17:06:47.951 spec-protocol> State 1: state invariant 10 holds. I@17:06:47.958 spec-protocol> State 1: state invariant 11 holds. I@17:06:47.965 spec-protocol> State 1: state invariant 12 holds. I@17:06:47.979 spec-protocol> State 1: state invariant 14 holds. I@17:06:47.996 spec-protocol> State 1: state invariant 15 holds. I@17:06:48.008 spec-protocol> State 1: state invariant 17 holds. I@17:06:48.021 spec-protocol> State 1: state invariant 18 holds. I@17:06:48.039 spec-protocol> State 1: state invariant 19 holds. I@17:06:48.061 spec-protocol> State 1: state invariant 20 holds. I@17:06:48.084 spec-protocol> State 1: state invariant 21 holds. I@17:06:48.117 spec-protocol> State 1: state invariant 23 holds. I@17:06:48.131 spec-protocol> State 1: state invariant 24 holds. I@17:06:48.140 spec-protocol> State 1: state invariant 26 holds. I@17:06:48.163 spec-protocol> State 1: state invariant 27 holds. I@17:06:48.259 spec-protocol> State 1: state invariant 28 holds. I@17:06:48.346 spec-protocol> State 1: state invariant 29 holds. I@17:06:48.376 spec-protocol> State 1: state invariant 30 holds. I@17:06:48.850 spec-protocol> State 1: state invariant 31 holds. I@17:06:49.457 spec-protocol> State 1: state invariant 32 holds. I@17:06:49.834 spec-protocol> Step 1: Transition #10 is disabled I@17:06:49.931 spec-protocol> Step 1: Transition #11 is disabled I@17:06:50.037 spec-protocol> State 1: Checking 27 state invariants I@17:06:50.585 spec-protocol> State 1: state invariant 0 holds. I@17:06:50.592 spec-protocol> State 1: state invariant 1 holds. I@17:06:50.686 spec-protocol> State 1: state invariant 9 holds. I@17:06:50.752 spec-protocol> State 1: state invariant 10 holds. I@17:06:50.757 spec-protocol> State 1: state invariant 12 holds. I@17:06:50.773 spec-protocol> State 1: state invariant 13 holds. I@17:06:50.781 spec-protocol> State 1: state invariant 14 holds. I@17:06:50.807 spec-protocol> State 1: state invariant 15 holds. I@17:06:50.882 spec-protocol> State 1: state invariant 16 holds. I@17:06:50.916 spec-protocol> State 1: state invariant 17 holds. I@17:06:50.933 spec-protocol> State 1: state invariant 18 holds. I@17:06:51.004 spec-protocol> State 1: state invariant 19 holds. I@17:06:51.034 spec-protocol> State 1: state invariant 20 holds. I@17:06:51.054 spec-protocol> State 1: state invariant 21 holds. I@17:06:51.080 spec-protocol> State 1: state invariant 22 holds. I@17:06:51.110 spec-protocol> State 1: state invariant 23 holds. I@17:06:51.153 spec-protocol> State 1: state invariant 24 holds. I@17:06:51.162 spec-protocol> State 1: state invariant 26 holds. I@17:06:51.193 spec-protocol> State 1: state invariant 27 holds. I@17:06:51.265 spec-protocol> State 1: state invariant 28 holds. I@17:06:51.365 spec-protocol> State 1: state invariant 29 holds. I@17:06:51.377 spec-protocol> State 1: state invariant 30 holds. I@17:06:51.625 spec-protocol> State 1: state invariant 31 holds. I@17:06:52.020 spec-protocol> State 1: state invariant 32 holds. I@17:06:52.364 spec-protocol> State 1: state invariant 33 holds. I@17:06:52.375 spec-protocol> State 1: state invariant 34 holds. I@17:06:52.397 spec-protocol> State 1: state invariant 35 holds. I@17:06:52.424 spec-protocol> State 1: Checking 23 state invariants I@17:06:52.804 spec-protocol> State 1: state invariant 0 holds. I@17:06:52.816 spec-protocol> State 1: state invariant 1 holds. I@17:06:52.868 spec-protocol> State 1: state invariant 9 holds. I@17:06:52.898 spec-protocol> State 1: state invariant 10 holds. I@17:06:52.907 spec-protocol> State 1: state invariant 12 holds. I@17:06:52.926 spec-protocol> State 1: state invariant 13 holds. I@17:06:52.935 spec-protocol> State 1: state invariant 14 holds. I@17:06:52.955 spec-protocol> State 1: state invariant 15 holds. I@17:06:52.981 spec-protocol> State 1: state invariant 16 holds. I@17:06:52.993 spec-protocol> State 1: state invariant 17 holds. I@17:06:53.003 spec-protocol> State 1: state invariant 18 holds. I@17:06:53.030 spec-protocol> State 1: state invariant 19 holds. I@17:06:53.116 spec-protocol> State 1: state invariant 20 holds. I@17:06:53.169 spec-protocol> State 1: state invariant 21 holds. I@17:06:53.212 spec-protocol> State 1: state invariant 23 holds. I@17:06:53.230 spec-protocol> State 1: state invariant 24 holds. I@17:06:53.238 spec-protocol> State 1: state invariant 26 holds. I@17:06:53.265 spec-protocol> State 1: state invariant 27 holds. I@17:06:53.288 spec-protocol> State 1: state invariant 28 holds. I@17:06:53.340 spec-protocol> State 1: state invariant 29 holds. I@17:06:53.356 spec-protocol> State 1: state invariant 30 holds. I@17:06:53.765 spec-protocol> State 1: state invariant 31 holds. I@17:06:54.142 spec-protocol> State 1: state invariant 32 holds. I@17:06:54.381 spec-protocol> State 1: Checking 26 state invariants I@17:06:54.733 spec-protocol> State 1: state invariant 0 holds. I@17:06:54.742 spec-protocol> State 1: state invariant 1 holds. I@17:06:54.791 spec-protocol> State 1: state invariant 9 holds. I@17:06:55.042 spec-protocol> State 1: state invariant 10 holds. I@17:06:55.052 spec-protocol> State 1: state invariant 12 holds. I@17:06:55.068 spec-protocol> State 1: state invariant 14 holds. I@17:06:55.087 spec-protocol> State 1: state invariant 15 holds. I@17:06:55.102 spec-protocol> State 1: state invariant 16 holds. I@17:06:55.113 spec-protocol> State 1: state invariant 17 holds. I@17:06:55.125 spec-protocol> State 1: state invariant 18 holds. I@17:06:55.159 spec-protocol> State 1: state invariant 19 holds. I@17:06:55.197 spec-protocol> State 1: state invariant 20 holds. I@17:06:55.218 spec-protocol> State 1: state invariant 21 holds. I@17:06:55.255 spec-protocol> State 1: state invariant 22 holds. I@17:06:55.297 spec-protocol> State 1: state invariant 23 holds. I@17:06:55.314 spec-protocol> State 1: state invariant 24 holds. I@17:06:55.324 spec-protocol> State 1: state invariant 26 holds. I@17:06:55.340 spec-protocol> State 1: state invariant 27 holds. I@17:06:55.372 spec-protocol> State 1: state invariant 28 holds. I@17:06:55.456 spec-protocol> State 1: state invariant 29 holds. I@17:06:55.472 spec-protocol> State 1: state invariant 30 holds. I@17:06:55.742 spec-protocol> State 1: state invariant 31 holds. I@17:06:56.050 spec-protocol> State 1: state invariant 32 holds. I@17:06:56.431 spec-protocol> State 1: state invariant 33 holds. I@17:06:56.575 spec-protocol> State 1: state invariant 34 holds. I@17:06:56.646 spec-protocol> State 1: state invariant 35 holds. I@17:06:56.695 spec-protocol> State 1: Checking 22 state invariants I@17:06:57.347 spec-protocol> State 1: state invariant 0 holds. I@17:06:57.357 spec-protocol> State 1: state invariant 1 holds. I@17:06:57.447 spec-protocol> State 1: state invariant 9 holds. I@17:06:57.484 spec-protocol> State 1: state invariant 10 holds. I@17:06:57.495 spec-protocol> State 1: state invariant 12 holds. I@17:06:57.519 spec-protocol> State 1: state invariant 14 holds. I@17:06:57.545 spec-protocol> State 1: state invariant 15 holds. I@17:06:57.562 spec-protocol> State 1: state invariant 16 holds. I@17:06:57.573 spec-protocol> State 1: state invariant 17 holds. I@17:06:57.583 spec-protocol> State 1: state invariant 18 holds. I@17:06:57.611 spec-protocol> State 1: state invariant 19 holds. I@17:06:57.653 spec-protocol> State 1: state invariant 20 holds. I@17:06:57.690 spec-protocol> State 1: state invariant 21 holds. I@17:06:57.747 spec-protocol> State 1: state invariant 23 holds. I@17:06:57.767 spec-protocol> State 1: state invariant 24 holds. I@17:06:57.778 spec-protocol> State 1: state invariant 26 holds. I@17:06:57.805 spec-protocol> State 1: state invariant 27 holds. I@17:06:57.869 spec-protocol> State 1: state invariant 28 holds. I@17:06:57.950 spec-protocol> State 1: state invariant 29 holds. I@17:06:57.970 spec-protocol> State 1: state invariant 30 holds. I@17:06:58.465 spec-protocol> State 1: state invariant 31 holds. I@17:06:58.750 spec-protocol> State 1: state invariant 32 holds. I@17:06:59.038 spec-protocol> Step 1: Transition #16 is disabled I@17:06:59.116 spec-protocol> State 1: Checking 21 state invariants I@17:06:59.240 spec-protocol> State 1: state invariant 0 holds. I@17:06:59.253 spec-protocol> State 1: state invariant 1 holds. I@17:06:59.329 spec-protocol> State 1: state invariant 9 holds. I@17:06:59.350 spec-protocol> State 1: state invariant 10 holds. I@17:06:59.361 spec-protocol> State 1: state invariant 12 holds. I@17:06:59.381 spec-protocol> State 1: state invariant 14 holds. I@17:06:59.407 spec-protocol> State 1: state invariant 15 holds. I@17:06:59.453 spec-protocol> State 1: state invariant 17 holds. I@17:06:59.464 spec-protocol> State 1: state invariant 18 holds. I@17:06:59.503 spec-protocol> State 1: state invariant 19 holds. I@17:06:59.529 spec-protocol> State 1: state invariant 20 holds. I@17:06:59.568 spec-protocol> State 1: state invariant 21 holds. I@17:06:59.650 spec-protocol> State 1: state invariant 23 holds. I@17:06:59.672 spec-protocol> State 1: state invariant 24 holds. I@17:06:59.685 spec-protocol> State 1: state invariant 26 holds. I@17:06:59.702 spec-protocol> State 1: state invariant 27 holds. I@17:06:59.741 spec-protocol> State 1: state invariant 28 holds. I@17:06:59.836 spec-protocol> State 1: state invariant 29 holds. I@17:06:59.858 spec-protocol> State 1: state invariant 30 holds. I@17:07:00.612 spec-protocol> State 1: state invariant 31 holds. I@17:07:01.050 spec-protocol> State 1: state invariant 32 holds. I@17:07:01.478 spec-protocol> Step 1: Transition #18 is disabled I@17:07:01.548 spec-protocol> State 1: Checking 21 state invariants I@17:07:01.764 spec-protocol> State 1: state invariant 0 holds. I@17:07:01.778 spec-protocol> State 1: state invariant 1 holds. I@17:07:01.827 spec-protocol> State 1: state invariant 9 holds. I@17:07:01.852 spec-protocol> State 1: state invariant 10 holds. I@17:07:01.862 spec-protocol> State 1: state invariant 12 holds. I@17:07:01.886 spec-protocol> State 1: state invariant 14 holds. I@17:07:01.907 spec-protocol> State 1: state invariant 15 holds. I@17:07:01.935 spec-protocol> State 1: state invariant 17 holds. I@17:07:01.946 spec-protocol> State 1: state invariant 18 holds. I@17:07:01.976 spec-protocol> State 1: state invariant 19 holds. I@17:07:02.021 spec-protocol> State 1: state invariant 20 holds. I@17:07:02.066 spec-protocol> State 1: state invariant 21 holds. I@17:07:02.151 spec-protocol> State 1: state invariant 23 holds. I@17:07:02.174 spec-protocol> State 1: state invariant 24 holds. I@17:07:02.186 spec-protocol> State 1: state invariant 26 holds. I@17:07:02.201 spec-protocol> State 1: state invariant 27 holds. I@17:07:02.326 spec-protocol> State 1: state invariant 28 holds. I@17:07:02.744 spec-protocol> State 1: state invariant 29 holds. I@17:07:02.767 spec-protocol> State 1: state invariant 30 holds. I@17:07:03.175 spec-protocol> State 1: state invariant 31 holds. I@17:07:03.687 spec-protocol> State 1: state invariant 32 holds. I@17:07:03.964 spec-protocol> Step 1: Transition #20 is disabled I@17:07:04.053 spec-protocol> Step 1: Transition #21 is disabled I@17:07:04.208 spec-protocol> State 1: Checking 14 state invariants I@17:07:04.544 spec-protocol> State 1: state invariant 6 holds. I@17:07:04.555 spec-protocol> State 1: state invariant 7 holds. I@17:07:04.565 spec-protocol> State 1: state invariant 22 holds. I@17:07:04.598 spec-protocol> State 1: state invariant 25 holds. I@17:07:04.610 spec-protocol> State 1: state invariant 27 holds. I@17:07:04.653 spec-protocol> State 1: state invariant 28 holds. I@17:07:04.694 spec-protocol> State 1: state invariant 29 holds. I@17:07:04.710 spec-protocol> State 1: state invariant 30 holds. I@17:07:04.904 spec-protocol> State 1: state invariant 31 holds. I@17:07:05.010 spec-protocol> State 1: state invariant 32 holds. I@17:07:05.184 spec-protocol> State 1: state invariant 33 holds. I@17:07:05.203 spec-protocol> State 1: state invariant 34 holds. I@17:07:05.219 spec-protocol> State 1: state invariant 35 holds. I@17:07:05.235 spec-protocol> State 1: state invariant 38 holds. I@17:07:05.244 spec-protocol> State 1: Checking 17 state invariants I@17:07:05.529 spec-protocol> State 1: state invariant 3 holds. I@17:07:05.542 spec-protocol> State 1: state invariant 4 holds. I@17:07:05.613 spec-protocol> State 1: state invariant 5 holds. I@17:07:05.732 spec-protocol> State 1: state invariant 6 holds. I@17:07:05.741 spec-protocol> State 1: state invariant 7 holds. I@17:07:05.749 spec-protocol> State 1: state invariant 22 holds. I@17:07:05.777 spec-protocol> State 1: state invariant 25 holds. I@17:07:05.786 spec-protocol> State 1: state invariant 27 holds. I@17:07:05.800 spec-protocol> State 1: state invariant 28 holds. I@17:07:06.059 spec-protocol> State 1: state invariant 29 holds. I@17:07:06.081 spec-protocol> State 1: state invariant 30 holds. I@17:07:07.208 spec-protocol> State 1: state invariant 31 holds. I@17:07:08.969 spec-protocol> State 1: state invariant 32 holds. I@17:07:11.075 spec-protocol> State 1: state invariant 33 holds. I@17:07:11.144 spec-protocol> State 1: state invariant 34 holds. I@17:07:11.157 spec-protocol> State 1: state invariant 35 holds. I@17:07:11.171 spec-protocol> State 1: state invariant 38 holds. I@17:07:11.178 spec-protocol> Step 1: picking a transition out of 17 transition(s) I@17:07:11.184 spec-protocol> The outcome is: NoError I@17:07:11.429 spec-protocol> > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... spec-protocol> PASS #0: SanyParser I@17:07:12.850 spec-protocol> PASS #1: TypeCheckerSnowcat I@17:07:13.039 spec-protocol> > Running Snowcat .::. I@17:07:13.042 spec-protocol> > Your types are purrfect! I@17:07:19.670 spec-protocol> > All expressions are typed I@17:07:19.670 spec-protocol> PASS #2: ConfigurationPass I@17:07:19.732 spec-protocol> > Set the initialization predicate to q::inductiveInv I@17:07:19.732 spec-protocol> > Set the transition predicate to q::step I@17:07:19.732 spec-protocol> > Set an invariant to q::inv I@17:07:19.733 spec-protocol> PASS #3: DesugarerPass I@17:07:19.735 spec-protocol> > Desugaring... I@17:07:19.735 spec-protocol> PASS #4: InlinePass I@17:07:19.738 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@17:07:19.738 spec-protocol> PASS #5: TemporalPass I@17:07:19.790 spec-protocol> > Rewriting temporal operators... I@17:07:19.791 spec-protocol> > No temporal property specified, nothing to encode I@17:07:19.809 spec-protocol> PASS #6: InlinePass I@17:07:19.810 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@17:07:19.810 spec-protocol> PASS #7: PrimingPass I@17:07:19.838 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@17:07:19.839 spec-protocol> PASS #8: VCGen I@17:07:19.840 spec-protocol> > Producing verification conditions from the invariant q::inv I@17:07:19.841 spec-protocol> > VCGen produced 5 verification condition(s) I@17:07:19.841 spec-protocol> PASS #9: PreprocessingPass I@17:07:19.841 spec-protocol> > Before preprocessing: unique renaming I@17:07:19.841 spec-protocol> > Applying standard transformations: I@17:07:19.841 spec-protocol> > PrimePropagation I@17:07:19.841 spec-protocol> > Desugarer I@17:07:19.851 spec-protocol> > UniqueRenamer I@17:07:19.858 spec-protocol> > Normalizer I@17:07:19.877 spec-protocol> > Keramelizer I@17:07:19.885 spec-protocol> > After preprocessing: UniqueRenamer I@17:07:19.905 spec-protocol> PASS #10: TransitionFinderPass I@17:07:19.937 spec-protocol> > Found 1 initializing transitions I@17:07:19.940 spec-protocol> > Found 24 transitions I@17:07:19.975 spec-protocol> > No constant initializer I@17:07:19.975 spec-protocol> > Applying unique renaming I@17:07:19.975 spec-protocol> PASS #11: OptimizationPass I@17:07:20.928 spec-protocol> > Applying optimizations: I@17:07:20.928 spec-protocol> > ConstSimplifier I@17:07:20.928 spec-protocol> > ExprOptimizer I@17:07:21.055 spec-protocol> > SetMembershipSimplifier I@17:07:21.100 spec-protocol> > ConstSimplifier I@17:07:21.114 spec-protocol> PASS #12: AnalysisPass I@17:07:21.756 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@17:07:21.839 spec-protocol> > Skolemization I@17:07:21.839 spec-protocol> > Expansion I@17:07:21.918 spec-protocol> > Remove unused let-in defs I@17:07:22.053 spec-protocol> > Running analyzers... I@17:07:22.074 spec-protocol> > Introduced expression grades I@17:07:22.088 spec-protocol> PASS #13: BoundedChecker I@17:07:22.088 spec-protocol> State 0: Checking 5 state invariants I@17:07:23.114 spec-protocol> State 0: state invariant 0 holds. I@17:07:23.116 spec-protocol> State 0: state invariant 1 holds. I@17:07:23.118 spec-protocol> State 0: state invariant 2 holds. I@17:07:23.122 spec-protocol> State 0: state invariant 3 holds. I@17:07:23.132 spec-protocol> State 0: state invariant 4 holds. I@17:07:23.207 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@17:07:23.213 spec-protocol> The outcome is: NoError I@17:07:23.242 spec-protocol> [ok] No violation found (114165ms). spec-protocol> You may increase --max-steps. spec-protocol> Use --verbosity to produce more (or less) output. warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy warning: SQLite database '/nix/var/nix/db/db.sqlite' is busy post-build step Upload coverage to codecov: ok Skipping codecov: project=Mic92/tribuchet attr=checks.x86_64-linux.spec-protocol