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-18T16-53-52_3792579933075861651 # APALACHE version: 0.62.1 | build: a321771 I@16:53:52.395 Starting checker server on port 8822... I@16:53:52.399 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:9f:b8:39:a6:c8:cd:4b W@16:53:53.093 Oct 18, 2026 4:53:56 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:53:57.535 PASS #1: TypeCheckerSnowcat I@16:53:58.294 > Running Snowcat .::. I@16:53:58.294 > Your types are purrfect! I@16:54:00.664 > All expressions are typed I@16:54:00.666 PASS #2: ConfigurationPass I@16:54:00.668 > Set the initialization predicate to q::init I@16:54:00.673 > Set the transition predicate to q::step I@16:54:00.674 > Set an invariant to q::inductiveInv I@16:54:00.674 PASS #3: DesugarerPass I@16:54:00.682 > Desugaring... I@16:54:00.682 PASS #4: InlinePass I@16:54:00.700 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:00.701 PASS #5: TemporalPass I@16:54:00.813 > Rewriting temporal operators... I@16:54:00.814 > No temporal property specified, nothing to encode I@16:54:00.814 PASS #6: InlinePass I@16:54:00.814 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@16:54:00.814 PASS #7: PrimingPass I@16:54:00.841 > Introducing q::initPrimed for q::init' I@16:54:00.844 PASS #8: VCGen I@16:54:00.845 > Producing verification conditions from the invariant q::inductiveInv I@16:54:00.846 > VCGen produced 39 verification condition(s) I@16:54:00.855 PASS #9: PreprocessingPass I@16:54:00.861 > Before preprocessing: unique renaming I@16:54:00.861 > Applying standard transformations: I@16:54:00.868 > PrimePropagation I@16:54:00.869 > Desugarer I@16:54:00.879 > UniqueRenamer I@16:54:00.887 > Normalizer I@16:54:00.914 > SetMembershipSimplifier I@16:54:00.936 > Keramelizer I@16:54:00.947 > After preprocessing: UniqueRenamer I@16:54:00.972 PASS #10: TransitionFinderPass I@16:54:01.019 > Found 1 initializing transitions I@16:54:01.033 > Found 24 transitions I@16:54:01.071 > No constant initializer I@16:54:01.072 > Applying unique renaming I@16:54:01.074 PASS #11: OptimizationPass I@16:54:01.106 > Applying optimizations: I@16:54:01.111 > ConstSimplifier I@16:54:01.112 > ExprOptimizer I@16:54:01.192 > SetMembershipSimplifier I@16:54:01.217 > ConstSimplifier I@16:54:01.224 PASS #12: AnalysisPass I@16:54:01.297 > Marking skolemizable existentials and sets to be expanded... I@16:54:01.301 > Skolemization I@16:54:01.301 > Expansion I@16:54:01.306 > Remove unused let-in defs I@16:54:01.325 > Running analyzers... I@16:54:01.337 > Introduced expression grades I@16:54:01.347 PASS #13: BoundedChecker I@16:54:01.348 State 0: Checking 39 state invariants I@16:54:01.820 State 0: state invariant 0 holds. I@16:54:01.826 State 0: state invariant 1 holds. I@16:54:01.874 State 0: state invariant 2 holds. I@16:54:01.875 State 0: state invariant 3 holds. I@16:54:01.876 State 0: state invariant 4 holds. I@16:54:01.906 State 0: state invariant 5 holds. I@16:54:01.911 State 0: state invariant 6 holds. I@16:54:01.913 State 0: state invariant 7 holds. I@16:54:01.914 State 0: state invariant 8 holds. I@16:54:01.915 State 0: state invariant 9 holds. I@16:54:01.923 State 0: state invariant 10 holds. I@16:54:01.924 State 0: state invariant 11 holds. I@16:54:01.924 State 0: state invariant 12 holds. I@16:54:01.935 State 0: state invariant 13 holds. I@16:54:01.936 State 0: state invariant 14 holds. I@16:54:01.944 State 0: state invariant 15 holds. I@16:54:01.945 State 0: state invariant 16 holds. I@16:54:01.945 State 0: state invariant 17 holds. I@16:54:01.946 State 0: state invariant 18 holds. I@16:54:01.948 State 0: state invariant 19 holds. I@16:54:01.952 State 0: state invariant 20 holds. I@16:54:01.957 State 0: state invariant 21 holds. I@16:54:01.963 State 0: state invariant 22 holds. I@16:54:01.967 State 0: state invariant 23 holds. I@16:54:01.974 State 0: state invariant 24 holds. I@16:54:01.977 State 0: state invariant 25 holds. I@16:54:01.977 State 0: state invariant 26 holds. I@16:54:01.982 State 0: state invariant 27 holds. I@16:54:01.990 State 0: state invariant 28 holds. I@16:54:02.006 State 0: state invariant 29 holds. I@16:54:02.014 State 0: state invariant 30 holds. I@16:54:02.036 State 0: state invariant 31 holds. I@16:54:02.071 State 0: state invariant 32 holds. I@16:54:02.098 State 0: state invariant 33 holds. I@16:54:02.099 State 0: state invariant 34 holds. I@16:54:02.104 State 0: state invariant 35 holds. I@16:54:02.108 State 0: state invariant 36 holds. I@16:54:02.109 State 0: state invariant 37 holds. I@16:54:02.110 State 0: state invariant 38 holds. I@16:54:02.110 Step 0: picking a transition out of 1 transition(s) I@16:54:02.111 The outcome is: NoError I@16:54:02.119 > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... PASS #0: SanyParser I@16:54:02.492 PASS #1: TypeCheckerSnowcat I@16:54:02.694 > Running Snowcat .::. I@16:54:02.694 > Your types are purrfect! I@16:54:04.907 > All expressions are typed I@16:54:04.908 PASS #2: ConfigurationPass I@16:54:04.908 > Set the initialization predicate to q::inductiveInv I@16:54:04.909 > Set the transition predicate to q::step I@16:54:04.909 > Set an invariant to q::inductiveInv I@16:54:04.909 PASS #3: DesugarerPass I@16:54:04.911 > Desugaring... I@16:54:04.911 PASS #4: InlinePass I@16:54:04.913 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:04.913 PASS #5: TemporalPass I@16:54:04.940 > Rewriting temporal operators... I@16:54:04.940 > No temporal property specified, nothing to encode I@16:54:04.940 PASS #6: InlinePass I@16:54:04.941 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@16:54:04.941 PASS #7: PrimingPass I@16:54:04.951 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:04.951 PASS #8: VCGen I@16:54:04.952 > Producing verification conditions from the invariant q::inductiveInv I@16:54:04.952 > VCGen produced 39 verification condition(s) I@16:54:04.953 PASS #9: PreprocessingPass I@16:54:04.956 > Before preprocessing: unique renaming I@16:54:04.956 > Applying standard transformations: I@16:54:04.956 > PrimePropagation I@16:54:04.956 > Desugarer I@16:54:04.959 > UniqueRenamer I@16:54:04.963 > Normalizer I@16:54:04.973 > SetMembershipSimplifier I@16:54:04.993 > Keramelizer I@16:54:04.997 > After preprocessing: UniqueRenamer I@16:54:05.007 PASS #10: TransitionFinderPass I@16:54:05.023 > Found 1 initializing transitions I@16:54:05.027 > Found 24 transitions I@16:54:05.037 > No constant initializer I@16:54:05.038 > Applying unique renaming I@16:54:05.038 PASS #11: OptimizationPass I@16:54:05.061 > Applying optimizations: I@16:54:05.062 > ConstSimplifier I@16:54:05.062 > ExprOptimizer I@16:54:05.148 > SetMembershipSimplifier I@16:54:05.167 > ConstSimplifier I@16:54:05.171 PASS #12: AnalysisPass I@16:54:05.243 > Marking skolemizable existentials and sets to be expanded... I@16:54:05.243 > Skolemization I@16:54:05.243 > Expansion I@16:54:05.248 > Remove unused let-in defs I@16:54:05.261 > Running analyzers... I@16:54:05.265 > Introduced expression grades I@16:54:05.267 PASS #13: BoundedChecker I@16:54:05.267 State 0: Checking 39 state invariants I@16:54:06.013 State 0: state invariant 0 holds. I@16:54:06.014 State 0: state invariant 1 holds. I@16:54:06.042 State 0: state invariant 2 holds. I@16:54:06.046 State 0: state invariant 3 holds. I@16:54:06.047 State 0: state invariant 4 holds. I@16:54:06.071 State 0: state invariant 5 holds. I@16:54:06.082 State 0: state invariant 6 holds. I@16:54:06.084 State 0: state invariant 7 holds. I@16:54:06.085 State 0: state invariant 8 holds. I@16:54:06.086 State 0: state invariant 9 holds. I@16:54:06.088 State 0: state invariant 10 holds. I@16:54:06.089 State 0: state invariant 11 holds. I@16:54:06.091 State 0: state invariant 12 holds. I@16:54:06.099 State 0: state invariant 13 holds. I@16:54:06.101 State 0: state invariant 14 holds. I@16:54:06.110 State 0: state invariant 15 holds. I@16:54:06.112 State 0: state invariant 16 holds. I@16:54:06.113 State 0: state invariant 17 holds. I@16:54:06.114 State 0: state invariant 18 holds. I@16:54:06.120 State 0: state invariant 19 holds. I@16:54:06.126 State 0: state invariant 20 holds. I@16:54:06.134 State 0: state invariant 21 holds. I@16:54:06.147 State 0: state invariant 22 holds. I@16:54:06.156 State 0: state invariant 23 holds. I@16:54:06.166 State 0: state invariant 24 holds. I@16:54:06.167 State 0: state invariant 25 holds. I@16:54:06.168 State 0: state invariant 26 holds. I@16:54:06.170 State 0: state invariant 27 holds. I@16:54:06.174 State 0: state invariant 28 holds. I@16:54:06.199 State 0: state invariant 29 holds. I@16:54:06.207 State 0: state invariant 30 holds. I@16:54:06.330 State 0: state invariant 31 holds. I@16:54:06.471 State 0: state invariant 32 holds. I@16:54:06.624 State 0: state invariant 33 holds. I@16:54:06.628 State 0: state invariant 34 holds. I@16:54:06.634 State 0: state invariant 35 holds. I@16:54:06.639 State 0: state invariant 36 holds. I@16:54:06.640 State 0: state invariant 37 holds. I@16:54:06.642 State 0: state invariant 38 holds. I@16:54:06.643 Step 0: picking a transition out of 1 transition(s) I@16:54:06.644 State 1: Checking 12 state invariants I@16:54:06.671 State 1: state invariant 0 holds. I@16:54:06.673 State 1: state invariant 1 holds. I@16:54:06.699 State 1: state invariant 18 holds. I@16:54:06.708 State 1: state invariant 19 holds. I@16:54:06.714 State 1: state invariant 20 holds. I@16:54:06.722 State 1: state invariant 21 holds. I@16:54:06.731 State 1: state invariant 27 holds. I@16:54:06.741 State 1: state invariant 28 holds. I@16:54:06.768 State 1: state invariant 29 holds. I@16:54:06.775 State 1: state invariant 30 holds. I@16:54:06.906 State 1: state invariant 31 holds. I@16:54:07.039 State 1: state invariant 32 holds. I@16:54:07.147 State 1: Checking 4 state invariants I@16:54:07.171 State 1: state invariant 13 holds. I@16:54:07.173 State 1: state invariant 29 holds. I@16:54:07.180 State 1: state invariant 30 holds. I@16:54:07.301 State 1: state invariant 31 holds. I@16:54:07.430 State 1: Checking 16 state invariants I@16:54:07.481 State 1: state invariant 0 holds. I@16:54:07.483 State 1: state invariant 1 holds. I@16:54:07.506 State 1: state invariant 3 holds. I@16:54:07.510 State 1: state invariant 4 holds. I@16:54:07.533 State 1: state invariant 5 holds. I@16:54:07.543 State 1: state invariant 18 holds. I@16:54:07.550 State 1: state invariant 19 holds. I@16:54:07.557 State 1: state invariant 20 holds. I@16:54:07.565 State 1: state invariant 21 holds. I@16:54:07.573 State 1: state invariant 23 holds. I@16:54:07.584 State 1: state invariant 27 holds. I@16:54:07.589 State 1: state invariant 28 holds. I@16:54:07.609 State 1: state invariant 29 holds. I@16:54:07.617 State 1: state invariant 30 holds. I@16:54:07.714 State 1: state invariant 31 holds. I@16:54:07.828 State 1: state invariant 32 holds. I@16:54:07.921 State 1: Checking 6 state invariants I@16:54:07.941 State 1: state invariant 2 holds. I@16:54:07.943 State 1: state invariant 27 holds. I@16:54:07.960 State 1: state invariant 29 holds. I@16:54:07.968 State 1: state invariant 30 holds. I@16:54:08.254 State 1: state invariant 31 holds. I@16:54:08.397 State 1: state invariant 38 holds. I@16:54:08.400 State 1: Checking 15 state invariants I@16:54:08.422 State 1: state invariant 0 holds. I@16:54:08.423 State 1: state invariant 1 holds. I@16:54:08.448 State 1: state invariant 2 holds. I@16:54:08.450 State 1: state invariant 12 holds. I@16:54:08.458 State 1: state invariant 18 holds. I@16:54:08.470 State 1: state invariant 19 holds. I@16:54:08.477 State 1: state invariant 20 holds. I@16:54:08.489 State 1: state invariant 21 holds. I@16:54:08.500 State 1: state invariant 27 holds. I@16:54:08.511 State 1: state invariant 28 holds. I@16:54:08.544 State 1: state invariant 29 holds. I@16:54:08.554 State 1: state invariant 30 holds. I@16:54:08.691 State 1: state invariant 31 holds. I@16:54:08.836 State 1: state invariant 32 holds. I@16:54:08.982 State 1: state invariant 37 holds. I@16:54:08.986 State 1: Checking 18 state invariants I@16:54:09.211 State 1: state invariant 9 holds. I@16:54:09.216 State 1: state invariant 10 holds. I@16:54:09.219 State 1: state invariant 11 holds. I@16:54:09.220 State 1: state invariant 14 holds. I@16:54:09.228 State 1: state invariant 15 holds. I@16:54:09.230 State 1: state invariant 17 holds. I@16:54:09.231 State 1: state invariant 22 holds. I@16:54:09.239 State 1: state invariant 24 holds. I@16:54:09.241 State 1: state invariant 26 holds. I@16:54:09.244 State 1: state invariant 27 holds. I@16:54:09.252 State 1: state invariant 28 holds. I@16:54:09.275 State 1: state invariant 29 holds. I@16:54:09.283 State 1: state invariant 30 holds. I@16:54:09.344 State 1: state invariant 31 holds. I@16:54:09.422 State 1: state invariant 32 holds. I@16:54:09.544 State 1: state invariant 33 holds. I@16:54:09.549 State 1: state invariant 34 holds. I@16:54:09.555 State 1: state invariant 35 holds. I@16:54:09.570 State 1: Checking 14 state invariants I@16:54:09.800 State 1: state invariant 9 holds. I@16:54:09.804 State 1: state invariant 10 holds. I@16:54:09.807 State 1: state invariant 11 holds. I@16:54:09.809 State 1: state invariant 14 holds. I@16:54:09.817 State 1: state invariant 15 holds. I@16:54:09.821 State 1: state invariant 17 holds. I@16:54:09.822 State 1: state invariant 24 holds. I@16:54:09.824 State 1: state invariant 26 holds. I@16:54:09.827 State 1: state invariant 27 holds. I@16:54:09.833 State 1: state invariant 28 holds. I@16:54:09.849 State 1: state invariant 29 holds. I@16:54:09.858 State 1: state invariant 30 holds. I@16:54:09.915 State 1: state invariant 31 holds. I@16:54:09.993 State 1: state invariant 32 holds. I@16:54:10.062 State 1: Checking 26 state invariants I@16:54:10.200 State 1: state invariant 0 holds. I@16:54:10.202 State 1: state invariant 1 holds. I@16:54:10.230 State 1: state invariant 9 holds. I@16:54:10.239 State 1: state invariant 10 holds. I@16:54:10.241 State 1: state invariant 11 holds. I@16:54:10.244 State 1: state invariant 12 holds. I@16:54:10.250 State 1: state invariant 14 holds. I@16:54:10.263 State 1: state invariant 15 holds. I@16:54:10.274 State 1: state invariant 17 holds. I@16:54:10.277 State 1: state invariant 18 holds. I@16:54:10.286 State 1: state invariant 19 holds. I@16:54:10.294 State 1: state invariant 20 holds. I@16:54:10.306 State 1: state invariant 21 holds. I@16:54:10.322 State 1: state invariant 22 holds. I@16:54:10.334 State 1: state invariant 23 holds. I@16:54:10.344 State 1: state invariant 24 holds. I@16:54:10.348 State 1: state invariant 26 holds. I@16:54:10.352 State 1: state invariant 27 holds. I@16:54:10.359 State 1: state invariant 28 holds. I@16:54:10.387 State 1: state invariant 29 holds. I@16:54:10.397 State 1: state invariant 30 holds. I@16:54:10.586 State 1: state invariant 31 holds. I@16:54:10.739 State 1: state invariant 32 holds. I@16:54:10.934 State 1: state invariant 33 holds. I@16:54:10.940 State 1: state invariant 34 holds. I@16:54:10.949 State 1: state invariant 35 holds. I@16:54:10.964 State 1: Checking 22 state invariants I@16:54:11.103 State 1: state invariant 0 holds. I@16:54:11.105 State 1: state invariant 1 holds. I@16:54:11.137 State 1: state invariant 9 holds. I@16:54:11.147 State 1: state invariant 10 holds. I@16:54:11.149 State 1: state invariant 11 holds. I@16:54:11.151 State 1: state invariant 12 holds. I@16:54:11.158 State 1: state invariant 14 holds. I@16:54:11.170 State 1: state invariant 15 holds. I@16:54:11.177 State 1: state invariant 17 holds. I@16:54:11.180 State 1: state invariant 18 holds. I@16:54:11.188 State 1: state invariant 19 holds. I@16:54:11.195 State 1: state invariant 20 holds. I@16:54:11.201 State 1: state invariant 21 holds. I@16:54:11.215 State 1: state invariant 23 holds. I@16:54:11.225 State 1: state invariant 24 holds. I@16:54:11.227 State 1: state invariant 26 holds. I@16:54:11.236 State 1: state invariant 27 holds. I@16:54:11.260 State 1: state invariant 28 holds. I@16:54:11.299 State 1: state invariant 29 holds. I@16:54:11.309 State 1: state invariant 30 holds. I@16:54:11.515 State 1: state invariant 31 holds. I@16:54:11.668 State 1: state invariant 32 holds. I@16:54:11.817 Step 1: Transition #10 is disabled I@16:54:11.861 Step 1: Transition #11 is disabled I@16:54:11.901 State 1: Checking 27 state invariants I@16:54:12.048 State 1: state invariant 0 holds. I@16:54:12.050 State 1: state invariant 1 holds. I@16:54:12.079 State 1: state invariant 9 holds. I@16:54:12.095 State 1: state invariant 10 holds. I@16:54:12.099 State 1: state invariant 12 holds. I@16:54:12.106 State 1: state invariant 13 holds. I@16:54:12.108 State 1: state invariant 14 holds. I@16:54:12.117 State 1: state invariant 15 holds. I@16:54:12.122 State 1: state invariant 16 holds. I@16:54:12.124 State 1: state invariant 17 holds. I@16:54:12.126 State 1: state invariant 18 holds. I@16:54:12.134 State 1: state invariant 19 holds. I@16:54:12.141 State 1: state invariant 20 holds. I@16:54:12.149 State 1: state invariant 21 holds. I@16:54:12.178 State 1: state invariant 22 holds. I@16:54:12.194 State 1: state invariant 23 holds. I@16:54:12.205 State 1: state invariant 24 holds. I@16:54:12.209 State 1: state invariant 26 holds. I@16:54:12.213 State 1: state invariant 27 holds. I@16:54:12.234 State 1: state invariant 28 holds. I@16:54:12.266 State 1: state invariant 29 holds. I@16:54:12.277 State 1: state invariant 30 holds. I@16:54:12.431 State 1: state invariant 31 holds. I@16:54:12.570 State 1: state invariant 32 holds. I@16:54:12.705 State 1: state invariant 33 holds. I@16:54:12.713 State 1: state invariant 34 holds. I@16:54:12.724 State 1: state invariant 35 holds. I@16:54:12.739 State 1: Checking 23 state invariants I@16:54:12.918 State 1: state invariant 0 holds. I@16:54:12.921 State 1: state invariant 1 holds. I@16:54:13.087 State 1: state invariant 9 holds. I@16:54:13.098 State 1: state invariant 10 holds. I@16:54:13.101 State 1: state invariant 12 holds. I@16:54:13.108 State 1: state invariant 13 holds. I@16:54:13.110 State 1: state invariant 14 holds. I@16:54:13.118 State 1: state invariant 15 holds. I@16:54:13.130 State 1: state invariant 16 holds. I@16:54:13.132 State 1: state invariant 17 holds. I@16:54:13.134 State 1: state invariant 18 holds. I@16:54:13.154 State 1: state invariant 19 holds. I@16:54:13.168 State 1: state invariant 20 holds. I@16:54:13.177 State 1: state invariant 21 holds. I@16:54:13.192 State 1: state invariant 23 holds. I@16:54:13.202 State 1: state invariant 24 holds. I@16:54:13.205 State 1: state invariant 26 holds. I@16:54:13.215 State 1: state invariant 27 holds. I@16:54:13.228 State 1: state invariant 28 holds. I@16:54:13.261 State 1: state invariant 29 holds. I@16:54:13.270 State 1: state invariant 30 holds. I@16:54:13.437 State 1: state invariant 31 holds. I@16:54:13.598 State 1: state invariant 32 holds. I@16:54:13.743 State 1: Checking 26 state invariants I@16:54:14.085 State 1: state invariant 0 holds. I@16:54:14.088 State 1: state invariant 1 holds. I@16:54:14.132 State 1: state invariant 9 holds. I@16:54:14.151 State 1: state invariant 10 holds. I@16:54:14.155 State 1: state invariant 12 holds. I@16:54:14.164 State 1: state invariant 14 holds. I@16:54:14.175 State 1: state invariant 15 holds. I@16:54:14.182 State 1: state invariant 16 holds. I@16:54:14.185 State 1: state invariant 17 holds. I@16:54:14.187 State 1: state invariant 18 holds. I@16:54:14.203 State 1: state invariant 19 holds. I@16:54:14.219 State 1: state invariant 20 holds. I@16:54:14.242 State 1: state invariant 21 holds. I@16:54:14.267 State 1: state invariant 22 holds. I@16:54:14.288 State 1: state invariant 23 holds. I@16:54:14.302 State 1: state invariant 24 holds. I@16:54:14.305 State 1: state invariant 26 holds. I@16:54:14.311 State 1: state invariant 27 holds. I@16:54:14.332 State 1: state invariant 28 holds. I@16:54:14.384 State 1: state invariant 29 holds. I@16:54:14.396 State 1: state invariant 30 holds. I@16:54:14.558 State 1: state invariant 31 holds. I@16:54:14.732 State 1: state invariant 32 holds. I@16:54:14.957 State 1: state invariant 33 holds. I@16:54:14.968 State 1: state invariant 34 holds. I@16:54:14.987 State 1: state invariant 35 holds. I@16:54:15.013 State 1: Checking 22 state invariants I@16:54:15.344 State 1: state invariant 0 holds. I@16:54:15.346 State 1: state invariant 1 holds. I@16:54:15.380 State 1: state invariant 9 holds. I@16:54:15.395 State 1: state invariant 10 holds. I@16:54:15.399 State 1: state invariant 12 holds. I@16:54:15.410 State 1: state invariant 14 holds. I@16:54:15.422 State 1: state invariant 15 holds. I@16:54:15.437 State 1: state invariant 16 holds. I@16:54:15.441 State 1: state invariant 17 holds. I@16:54:15.444 State 1: state invariant 18 holds. I@16:54:15.455 State 1: state invariant 19 holds. I@16:54:15.480 State 1: state invariant 20 holds. I@16:54:15.496 State 1: state invariant 21 holds. I@16:54:15.518 State 1: state invariant 23 holds. I@16:54:15.532 State 1: state invariant 24 holds. I@16:54:15.536 State 1: state invariant 26 holds. I@16:54:15.548 State 1: state invariant 27 holds. I@16:54:15.575 State 1: state invariant 28 holds. I@16:54:15.607 State 1: state invariant 29 holds. I@16:54:15.618 State 1: state invariant 30 holds. I@16:54:15.791 State 1: state invariant 31 holds. I@16:54:15.935 State 1: state invariant 32 holds. I@16:54:16.063 Step 1: Transition #16 is disabled I@16:54:16.158 State 1: Checking 21 state invariants I@16:54:16.250 State 1: state invariant 0 holds. I@16:54:16.252 State 1: state invariant 1 holds. I@16:54:16.297 State 1: state invariant 9 holds. I@16:54:16.311 State 1: state invariant 10 holds. I@16:54:16.315 State 1: state invariant 12 holds. I@16:54:16.326 State 1: state invariant 14 holds. I@16:54:16.339 State 1: state invariant 15 holds. I@16:54:16.348 State 1: state invariant 17 holds. I@16:54:16.352 State 1: state invariant 18 holds. I@16:54:16.368 State 1: state invariant 19 holds. I@16:54:16.388 State 1: state invariant 20 holds. I@16:54:16.410 State 1: state invariant 21 holds. I@16:54:16.440 State 1: state invariant 23 holds. I@16:54:16.454 State 1: state invariant 24 holds. I@16:54:16.459 State 1: state invariant 26 holds. I@16:54:16.463 State 1: state invariant 27 holds. I@16:54:16.478 State 1: state invariant 28 holds. I@16:54:16.515 State 1: state invariant 29 holds. I@16:54:16.527 State 1: state invariant 30 holds. I@16:54:16.744 State 1: state invariant 31 holds. I@16:54:16.982 State 1: state invariant 32 holds. I@16:54:17.155 Step 1: Transition #18 is disabled I@16:54:17.209 State 1: Checking 21 state invariants I@16:54:17.284 State 1: state invariant 0 holds. I@16:54:17.285 State 1: state invariant 1 holds. I@16:54:17.321 State 1: state invariant 9 holds. I@16:54:17.334 State 1: state invariant 10 holds. I@16:54:17.337 State 1: state invariant 12 holds. I@16:54:17.346 State 1: state invariant 14 holds. I@16:54:17.358 State 1: state invariant 15 holds. I@16:54:17.364 State 1: state invariant 17 holds. I@16:54:17.366 State 1: state invariant 18 holds. I@16:54:17.377 State 1: state invariant 19 holds. I@16:54:17.393 State 1: state invariant 20 holds. I@16:54:17.405 State 1: state invariant 21 holds. I@16:54:17.427 State 1: state invariant 23 holds. I@16:54:17.440 State 1: state invariant 24 holds. I@16:54:17.444 State 1: state invariant 26 holds. I@16:54:17.449 State 1: state invariant 27 holds. I@16:54:17.477 State 1: state invariant 28 holds. I@16:54:17.536 State 1: state invariant 29 holds. I@16:54:17.547 State 1: state invariant 30 holds. I@16:54:17.803 State 1: state invariant 31 holds. I@16:54:18.090 State 1: state invariant 32 holds. I@16:54:18.297 Step 1: Transition #20 is disabled I@16:54:18.351 Step 1: Transition #21 is disabled I@16:54:18.418 State 1: Checking 14 state invariants I@16:54:18.525 State 1: state invariant 6 holds. I@16:54:18.527 State 1: state invariant 7 holds. I@16:54:18.531 State 1: state invariant 22 holds. I@16:54:18.552 State 1: state invariant 25 holds. I@16:54:18.563 State 1: state invariant 27 holds. I@16:54:18.603 State 1: state invariant 28 holds. I@16:54:18.644 State 1: state invariant 29 holds. I@16:54:18.654 State 1: state invariant 30 holds. I@16:54:18.843 State 1: state invariant 31 holds. I@16:54:18.950 State 1: state invariant 32 holds. I@16:54:19.079 State 1: state invariant 33 holds. I@16:54:19.086 State 1: state invariant 34 holds. I@16:54:19.094 State 1: state invariant 35 holds. I@16:54:19.101 State 1: state invariant 38 holds. I@16:54:19.104 State 1: Checking 17 state invariants I@16:54:19.187 State 1: state invariant 3 holds. I@16:54:19.191 State 1: state invariant 4 holds. I@16:54:19.243 State 1: state invariant 5 holds. I@16:54:19.284 State 1: state invariant 6 holds. I@16:54:19.287 State 1: state invariant 7 holds. I@16:54:19.289 State 1: state invariant 22 holds. I@16:54:19.305 State 1: state invariant 25 holds. I@16:54:19.308 State 1: state invariant 27 holds. I@16:54:19.314 State 1: state invariant 28 holds. I@16:54:19.348 State 1: state invariant 29 holds. I@16:54:19.357 State 1: state invariant 30 holds. I@16:54:19.610 State 1: state invariant 31 holds. I@16:54:19.780 State 1: state invariant 32 holds. I@16:54:20.009 State 1: state invariant 33 holds. I@16:54:20.020 State 1: state invariant 34 holds. I@16:54:20.029 State 1: state invariant 35 holds. I@16:54:20.037 State 1: state invariant 38 holds. I@16:54:20.040 Step 1: picking a transition out of 17 transition(s) I@16:54:20.042 The outcome is: NoError I@16:54:20.491 > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... PASS #0: SanyParser I@16:54:20.719 PASS #1: TypeCheckerSnowcat I@16:54:20.849 > Running Snowcat .::. I@16:54:20.850 > Your types are purrfect! I@16:54:22.818 > All expressions are typed I@16:54:22.818 PASS #2: ConfigurationPass I@16:54:22.819 > Set the initialization predicate to q::inductiveInv I@16:54:22.819 > Set the transition predicate to q::step I@16:54:22.819 > Set an invariant to q::inv I@16:54:22.820 PASS #3: DesugarerPass I@16:54:22.821 > Desugaring... I@16:54:22.821 PASS #4: InlinePass I@16:54:22.823 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:54:22.823 PASS #5: TemporalPass I@16:54:22.849 > Rewriting temporal operators... I@16:54:22.849 > No temporal property specified, nothing to encode I@16:54:22.849 PASS #6: InlinePass I@16:54:22.849 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@16:54:22.849 PASS #7: PrimingPass I@16:54:22.860 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@16:54:22.860 PASS #8: VCGen I@16:54:22.861 > Producing verification conditions from the invariant q::inv I@16:54:22.861 > VCGen produced 5 verification condition(s) I@16:54:22.861 PASS #9: PreprocessingPass I@16:54:22.862 > Before preprocessing: unique renaming I@16:54:22.862 > Applying standard transformations: I@16:54:22.862 > PrimePropagation I@16:54:22.862 > Desugarer I@16:54:22.866 > UniqueRenamer I@16:54:22.870 > Normalizer I@16:54:22.879 > SetMembershipSimplifier I@16:54:22.884 > Keramelizer I@16:54:22.887 > After preprocessing: UniqueRenamer I@16:54:22.895 PASS #10: TransitionFinderPass I@16:54:22.907 > Found 1 initializing transitions I@16:54:22.909 > Found 24 transitions I@16:54:22.918 > No constant initializer I@16:54:22.919 > Applying unique renaming I@16:54:22.919 PASS #11: OptimizationPass I@16:54:22.935 > Applying optimizations: I@16:54:22.935 > ConstSimplifier I@16:54:22.935 > ExprOptimizer I@16:54:22.995 > SetMembershipSimplifier I@16:54:23.002 > ConstSimplifier I@16:54:23.006 PASS #12: AnalysisPass I@16:54:23.063 > Marking skolemizable existentials and sets to be expanded... I@16:54:23.063 > Skolemization I@16:54:23.063 > Expansion I@16:54:23.066 > Remove unused let-in defs I@16:54:23.078 > Running analyzers... I@16:54:23.081 > Introduced expression grades I@16:54:23.082 PASS #13: BoundedChecker I@16:54:23.083 State 0: Checking 5 state invariants I@16:54:23.624 State 0: state invariant 0 holds. I@16:54:23.625 State 0: state invariant 1 holds. I@16:54:23.626 State 0: state invariant 2 holds. I@16:54:23.628 State 0: state invariant 3 holds. I@16:54:23.632 State 0: state invariant 4 holds. I@16:54:23.663 Step 0: picking a transition out of 1 transition(s) I@16:54:23.666 The outcome is: NoError I@16:54:23.680 [ok] No violation found (31962ms). You may increase --max-steps. Use --verbosity to produce more (or less) output.