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