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