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