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-08-25T08-54-50_4577010489392133844 # APALACHE version: 0.56.1 | build: 70cdaf4 I@08:54:50.762 Starting checker server on port 8822... I@08:54:50.772 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: 21:b9:05:1d:0a:d1:e1:58 W@08:54:51.479 Aug 25, 2026 8:54:54 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@08:54:54.660 PASS #1: TypeCheckerSnowcat I@08:54:55.261 > Running Snowcat .::. I@08:54:55.261 > Your types are purrfect! I@08:54:57.259 > All expressions are typed I@08:54:57.260 PASS #2: ConfigurationPass I@08:54:57.261 > Set the initialization predicate to q::init I@08:54:57.267 > Set the transition predicate to q::step I@08:54:57.267 > Set an invariant to q::inductiveInv I@08:54:57.267 PASS #3: DesugarerPass I@08:54:57.274 > Desugaring... I@08:54:57.274 PASS #4: InlinePass I@08:54:57.290 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@08:54:57.290 PASS #5: TemporalPass I@08:54:57.384 > Rewriting temporal operators... I@08:54:57.384 > No temporal property specified, nothing to encode I@08:54:57.384 PASS #6: InlinePass I@08:54:57.384 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@08:54:57.384 PASS #7: PrimingPass I@08:54:57.403 > Introducing q::initPrimed for q::init' I@08:54:57.405 PASS #8: VCGen I@08:54:57.406 > Producing verification conditions from the invariant q::inductiveInv I@08:54:57.406 > VCGen produced 35 verification condition(s) I@08:54:57.415 PASS #9: PreprocessingPass I@08:54:57.418 > Before preprocessing: unique renaming I@08:54:57.418 > Applying standard transformations: I@08:54:57.424 > PrimePropagation I@08:54:57.424 > Desugarer I@08:54:57.429 > UniqueRenamer I@08:54:57.438 > Normalizer I@08:54:57.457 > Keramelizer I@08:54:57.472 > After preprocessing: UniqueRenamer I@08:54:57.495 PASS #10: TransitionFinderPass I@08:54:57.527 > Found 1 initializing transitions I@08:54:57.540 > Found 18 transitions I@08:54:57.568 > No constant initializer I@08:54:57.569 > Applying unique renaming I@08:54:57.570 PASS #11: OptimizationPass I@08:54:57.590 > Applying optimizations: I@08:54:57.597 > ConstSimplifier I@08:54:57.598 > ExprOptimizer I@08:54:57.650 > SetMembershipSimplifier I@08:54:57.674 > ConstSimplifier I@08:54:57.683 PASS #12: AnalysisPass I@08:54:57.731 > Marking skolemizable existentials and sets to be expanded... I@08:54:57.734 > Skolemization I@08:54:57.734 > Expansion I@08:54:57.739 > Remove unused let-in defs I@08:54:57.754 > Running analyzers... I@08:54:57.765 > Introduced expression grades I@08:54:57.775 PASS #13: BoundedChecker I@08:54:57.775 State 0: Checking 35 state invariants I@08:54:58.170 State 0: state invariant 0 holds. I@08:54:58.172 State 0: state invariant 1 holds. I@08:54:58.213 State 0: state invariant 2 holds. I@08:54:58.215 State 0: state invariant 3 holds. I@08:54:58.217 State 0: state invariant 4 holds. I@08:54:58.218 State 0: state invariant 5 holds. I@08:54:58.227 State 0: state invariant 6 holds. I@08:54:58.227 State 0: state invariant 7 holds. I@08:54:58.228 State 0: state invariant 8 holds. I@08:54:58.229 State 0: state invariant 9 holds. I@08:54:58.238 State 0: state invariant 10 holds. I@08:54:58.239 State 0: state invariant 11 holds. I@08:54:58.240 State 0: state invariant 12 holds. I@08:54:58.250 State 0: state invariant 13 holds. I@08:54:58.250 State 0: state invariant 14 holds. I@08:54:58.255 State 0: state invariant 15 holds. I@08:54:58.259 State 0: state invariant 16 holds. I@08:54:58.264 State 0: state invariant 17 holds. I@08:54:58.274 State 0: state invariant 18 holds. I@08:54:58.279 State 0: state invariant 19 holds. I@08:54:58.282 State 0: state invariant 20 holds. I@08:54:58.283 State 0: state invariant 21 holds. I@08:54:58.288 State 0: state invariant 22 holds. I@08:54:58.297 State 0: state invariant 23 holds. I@08:54:58.304 State 0: state invariant 24 holds. I@08:54:58.362 State 0: state invariant 25 holds. I@08:54:58.370 State 0: state invariant 26 holds. I@08:54:58.392 State 0: state invariant 27 holds. I@08:54:58.420 State 0: state invariant 28 holds. I@08:54:58.448 State 0: state invariant 29 holds. I@08:54:58.449 State 0: state invariant 30 holds. I@08:54:58.461 State 0: state invariant 31 holds. I@08:54:58.472 State 0: state invariant 32 holds. I@08:54:58.473 State 0: state invariant 33 holds. I@08:54:58.474 State 0: state invariant 34 holds. I@08:54:58.475 Step 0: picking a transition out of 1 transition(s) I@08:54:58.475 The outcome is: NoError I@08:54:58.491 > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... PASS #0: SanyParser I@08:54:58.840 PASS #1: TypeCheckerSnowcat I@08:54:58.941 > Running Snowcat .::. I@08:54:58.941 > Your types are purrfect! I@08:55:00.778 > All expressions are typed I@08:55:00.779 PASS #2: ConfigurationPass I@08:55:00.779 > Set the initialization predicate to q::inductiveInv I@08:55:00.779 > Set the transition predicate to q::step I@08:55:00.780 > Set an invariant to q::inductiveInv I@08:55:00.780 PASS #3: DesugarerPass I@08:55:00.781 > Desugaring... I@08:55:00.782 PASS #4: InlinePass I@08:55:00.784 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@08:55:00.784 PASS #5: TemporalPass I@08:55:00.811 > Rewriting temporal operators... I@08:55:00.811 > No temporal property specified, nothing to encode I@08:55:00.811 PASS #6: InlinePass I@08:55:00.811 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@08:55:00.811 PASS #7: PrimingPass I@08:55:00.821 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@08:55:00.821 PASS #8: VCGen I@08:55:00.822 > Producing verification conditions from the invariant q::inductiveInv I@08:55:00.823 > VCGen produced 35 verification condition(s) I@08:55:00.823 PASS #9: PreprocessingPass I@08:55:00.824 > Before preprocessing: unique renaming I@08:55:00.824 > Applying standard transformations: I@08:55:00.824 > PrimePropagation I@08:55:00.824 > Desugarer I@08:55:00.828 > UniqueRenamer I@08:55:00.834 > Normalizer I@08:55:00.843 > Keramelizer I@08:55:00.857 > After preprocessing: UniqueRenamer I@08:55:00.868 PASS #10: TransitionFinderPass I@08:55:00.880 > Found 1 initializing transitions I@08:55:00.883 > Found 18 transitions I@08:55:00.892 > No constant initializer I@08:55:00.892 > Applying unique renaming I@08:55:00.893 PASS #11: OptimizationPass I@08:55:00.910 > Applying optimizations: I@08:55:00.910 > ConstSimplifier I@08:55:00.911 > ExprOptimizer I@08:55:00.971 > SetMembershipSimplifier I@08:55:00.984 > ConstSimplifier I@08:55:00.988 PASS #12: AnalysisPass I@08:55:01.043 > Marking skolemizable existentials and sets to be expanded... I@08:55:01.043 > Skolemization I@08:55:01.043 > Expansion I@08:55:01.046 > Remove unused let-in defs I@08:55:01.054 > Running analyzers... I@08:55:01.057 > Introduced expression grades I@08:55:01.059 PASS #13: BoundedChecker I@08:55:01.060 State 0: Checking 35 state invariants I@08:55:01.557 State 0: state invariant 0 holds. I@08:55:01.558 State 0: state invariant 1 holds. I@08:55:01.576 State 0: state invariant 2 holds. I@08:55:01.578 State 0: state invariant 3 holds. I@08:55:01.579 State 0: state invariant 4 holds. I@08:55:01.580 State 0: state invariant 5 holds. I@08:55:01.584 State 0: state invariant 6 holds. I@08:55:01.585 State 0: state invariant 7 holds. I@08:55:01.586 State 0: state invariant 8 holds. I@08:55:01.588 State 0: state invariant 9 holds. I@08:55:01.595 State 0: state invariant 10 holds. I@08:55:01.596 State 0: state invariant 11 holds. I@08:55:01.597 State 0: state invariant 12 holds. I@08:55:01.603 State 0: state invariant 13 holds. I@08:55:01.605 State 0: state invariant 14 holds. I@08:55:01.609 State 0: state invariant 15 holds. I@08:55:01.615 State 0: state invariant 16 holds. I@08:55:01.626 State 0: state invariant 17 holds. I@08:55:01.637 State 0: state invariant 18 holds. I@08:55:01.646 State 0: state invariant 19 holds. I@08:55:01.647 State 0: state invariant 20 holds. I@08:55:01.647 State 0: state invariant 21 holds. I@08:55:01.648 State 0: state invariant 22 holds. I@08:55:01.653 State 0: state invariant 23 holds. I@08:55:01.660 State 0: state invariant 24 holds. I@08:55:01.716 State 0: state invariant 25 holds. I@08:55:01.722 State 0: state invariant 26 holds. I@08:55:01.824 State 0: state invariant 27 holds. I@08:55:01.890 State 0: state invariant 28 holds. I@08:55:02.014 State 0: state invariant 29 holds. I@08:55:02.017 State 0: state invariant 30 holds. I@08:55:02.030 State 0: state invariant 31 holds. I@08:55:02.045 State 0: state invariant 32 holds. I@08:55:02.046 State 0: state invariant 33 holds. I@08:55:02.047 State 0: state invariant 34 holds. I@08:55:02.048 Step 0: picking a transition out of 1 transition(s) I@08:55:02.048 State 1: Checking 4 state invariants I@08:55:02.061 State 1: state invariant 8 holds. I@08:55:02.062 State 1: state invariant 25 holds. I@08:55:02.067 State 1: state invariant 26 holds. I@08:55:02.180 State 1: state invariant 27 holds. I@08:55:02.249 State 1: Checking 15 state invariants I@08:55:02.264 State 1: state invariant 0 holds. I@08:55:02.265 State 1: state invariant 1 holds. I@08:55:02.282 State 1: state invariant 12 holds. I@08:55:02.290 State 1: state invariant 14 holds. I@08:55:02.297 State 1: state invariant 15 holds. I@08:55:02.303 State 1: state invariant 16 holds. I@08:55:02.310 State 1: state invariant 17 holds. I@08:55:02.321 State 1: state invariant 22 holds. I@08:55:02.329 State 1: state invariant 24 holds. I@08:55:02.380 State 1: state invariant 25 holds. I@08:55:02.387 State 1: state invariant 26 holds. I@08:55:02.472 State 1: state invariant 27 holds. I@08:55:02.544 State 1: state invariant 28 holds. I@08:55:02.627 State 1: state invariant 33 holds. I@08:55:02.630 State 1: state invariant 34 holds. I@08:55:02.631 State 1: Checking 18 state invariants I@08:55:02.773 State 1: state invariant 5 holds. I@08:55:02.777 State 1: state invariant 6 holds. I@08:55:02.779 State 1: state invariant 7 holds. I@08:55:02.780 State 1: state invariant 9 holds. I@08:55:02.786 State 1: state invariant 10 holds. I@08:55:02.787 State 1: state invariant 13 holds. I@08:55:02.788 State 1: state invariant 18 holds. I@08:55:02.797 State 1: state invariant 19 holds. I@08:55:02.799 State 1: state invariant 21 holds. I@08:55:02.801 State 1: state invariant 22 holds. I@08:55:02.809 State 1: state invariant 24 holds. I@08:55:02.849 State 1: state invariant 25 holds. I@08:55:02.856 State 1: state invariant 26 holds. I@08:55:02.903 State 1: state invariant 27 holds. I@08:55:02.938 State 1: state invariant 28 holds. I@08:55:03.002 State 1: state invariant 29 holds. I@08:55:03.005 State 1: state invariant 30 holds. I@08:55:03.018 State 1: state invariant 31 holds. I@08:55:03.057 State 1: Checking 14 state invariants I@08:55:03.169 State 1: state invariant 5 holds. I@08:55:03.172 State 1: state invariant 6 holds. I@08:55:03.174 State 1: state invariant 7 holds. I@08:55:03.175 State 1: state invariant 9 holds. I@08:55:03.181 State 1: state invariant 10 holds. I@08:55:03.183 State 1: state invariant 13 holds. I@08:55:03.184 State 1: state invariant 19 holds. I@08:55:03.185 State 1: state invariant 21 holds. I@08:55:03.187 State 1: state invariant 22 holds. I@08:55:03.192 State 1: state invariant 24 holds. I@08:55:03.212 State 1: state invariant 25 holds. I@08:55:03.218 State 1: state invariant 26 holds. I@08:55:03.262 State 1: state invariant 27 holds. I@08:55:03.295 State 1: state invariant 28 holds. I@08:55:03.338 State 1: Checking 26 state invariants I@08:55:03.434 State 1: state invariant 0 holds. I@08:55:03.435 State 1: state invariant 1 holds. I@08:55:03.454 State 1: state invariant 5 holds. I@08:55:03.459 State 1: state invariant 6 holds. I@08:55:03.460 State 1: state invariant 7 holds. I@08:55:03.462 State 1: state invariant 9 holds. I@08:55:03.469 State 1: state invariant 10 holds. I@08:55:03.480 State 1: state invariant 12 holds. I@08:55:03.487 State 1: state invariant 13 holds. I@08:55:03.488 State 1: state invariant 14 holds. I@08:55:03.497 State 1: state invariant 15 holds. I@08:55:03.504 State 1: state invariant 16 holds. I@08:55:03.509 State 1: state invariant 17 holds. I@08:55:03.519 State 1: state invariant 18 holds. I@08:55:03.539 State 1: state invariant 19 holds. I@08:55:03.541 State 1: state invariant 21 holds. I@08:55:03.544 State 1: state invariant 22 holds. I@08:55:03.564 State 1: state invariant 23 holds. I@08:55:03.571 State 1: state invariant 24 holds. I@08:55:03.643 State 1: state invariant 25 holds. I@08:55:03.650 State 1: state invariant 26 holds. I@08:55:03.738 State 1: state invariant 27 holds. I@08:55:03.804 State 1: state invariant 28 holds. I@08:55:04.075 State 1: state invariant 29 holds. I@08:55:04.079 State 1: state invariant 30 holds. I@08:55:04.094 State 1: state invariant 31 holds. I@08:55:04.143 State 1: Checking 22 state invariants I@08:55:04.243 State 1: state invariant 0 holds. I@08:55:04.244 State 1: state invariant 1 holds. I@08:55:04.262 State 1: state invariant 5 holds. I@08:55:04.268 State 1: state invariant 6 holds. I@08:55:04.269 State 1: state invariant 7 holds. I@08:55:04.270 State 1: state invariant 9 holds. I@08:55:04.278 State 1: state invariant 10 holds. I@08:55:04.282 State 1: state invariant 12 holds. I@08:55:04.287 State 1: state invariant 13 holds. I@08:55:04.289 State 1: state invariant 14 holds. I@08:55:04.295 State 1: state invariant 15 holds. I@08:55:04.303 State 1: state invariant 16 holds. I@08:55:04.311 State 1: state invariant 17 holds. I@08:55:04.325 State 1: state invariant 19 holds. I@08:55:04.326 State 1: state invariant 21 holds. I@08:55:04.330 State 1: state invariant 22 holds. I@08:55:04.340 State 1: state invariant 23 holds. I@08:55:04.347 State 1: state invariant 24 holds. I@08:55:04.394 State 1: state invariant 25 holds. I@08:55:04.401 State 1: state invariant 26 holds. I@08:55:04.519 State 1: state invariant 27 holds. I@08:55:04.587 State 1: state invariant 28 holds. I@08:55:04.670 Step 1: Transition #6 is disabled I@08:55:04.706 Step 1: Transition #7 is disabled I@08:55:04.735 State 1: Checking 27 state invariants I@08:55:04.826 State 1: state invariant 0 holds. I@08:55:04.827 State 1: state invariant 1 holds. I@08:55:04.840 State 1: state invariant 5 holds. I@08:55:04.847 State 1: state invariant 6 holds. I@08:55:04.849 State 1: state invariant 8 holds. I@08:55:04.850 State 1: state invariant 9 holds. I@08:55:04.855 State 1: state invariant 10 holds. I@08:55:04.859 State 1: state invariant 11 holds. I@08:55:04.860 State 1: state invariant 12 holds. I@08:55:04.865 State 1: state invariant 13 holds. I@08:55:04.866 State 1: state invariant 14 holds. I@08:55:04.870 State 1: state invariant 15 holds. I@08:55:04.884 State 1: state invariant 16 holds. I@08:55:04.889 State 1: state invariant 17 holds. I@08:55:04.897 State 1: state invariant 18 holds. I@08:55:04.915 State 1: state invariant 19 holds. I@08:55:04.917 State 1: state invariant 21 holds. I@08:55:04.919 State 1: state invariant 22 holds. I@08:55:04.931 State 1: state invariant 23 holds. I@08:55:04.938 State 1: state invariant 24 holds. I@08:55:04.988 State 1: state invariant 25 holds. I@08:55:04.995 State 1: state invariant 26 holds. I@08:55:05.080 State 1: state invariant 27 holds. I@08:55:05.150 State 1: state invariant 28 holds. I@08:55:05.265 State 1: state invariant 29 holds. I@08:55:05.268 State 1: state invariant 30 holds. I@08:55:05.287 State 1: state invariant 31 holds. I@08:55:05.332 State 1: Checking 23 state invariants I@08:55:05.418 State 1: state invariant 0 holds. I@08:55:05.419 State 1: state invariant 1 holds. I@08:55:05.434 State 1: state invariant 5 holds. I@08:55:05.440 State 1: state invariant 6 holds. I@08:55:05.441 State 1: state invariant 8 holds. I@08:55:05.443 State 1: state invariant 9 holds. I@08:55:05.448 State 1: state invariant 10 holds. I@08:55:05.453 State 1: state invariant 11 holds. I@08:55:05.454 State 1: state invariant 12 holds. I@08:55:05.458 State 1: state invariant 13 holds. I@08:55:05.459 State 1: state invariant 14 holds. I@08:55:05.464 State 1: state invariant 15 holds. I@08:55:05.471 State 1: state invariant 16 holds. I@08:55:05.478 State 1: state invariant 17 holds. I@08:55:05.486 State 1: state invariant 19 holds. I@08:55:05.488 State 1: state invariant 21 holds. I@08:55:05.491 State 1: state invariant 22 holds. I@08:55:05.498 State 1: state invariant 23 holds. I@08:55:05.505 State 1: state invariant 24 holds. I@08:55:05.538 State 1: state invariant 25 holds. I@08:55:05.545 State 1: state invariant 26 holds. I@08:55:05.656 State 1: state invariant 27 holds. I@08:55:05.719 State 1: state invariant 28 holds. I@08:55:05.808 State 1: Checking 26 state invariants I@08:55:05.977 State 1: state invariant 0 holds. I@08:55:05.979 State 1: state invariant 1 holds. I@08:55:05.995 State 1: state invariant 5 holds. I@08:55:06.004 State 1: state invariant 6 holds. I@08:55:06.005 State 1: state invariant 9 holds. I@08:55:06.011 State 1: state invariant 10 holds. I@08:55:06.014 State 1: state invariant 11 holds. I@08:55:06.015 State 1: state invariant 12 holds. I@08:55:06.020 State 1: state invariant 13 holds. I@08:55:06.021 State 1: state invariant 14 holds. I@08:55:06.038 State 1: state invariant 15 holds. I@08:55:06.046 State 1: state invariant 16 holds. I@08:55:06.053 State 1: state invariant 17 holds. I@08:55:06.068 State 1: state invariant 18 holds. I@08:55:06.086 State 1: state invariant 19 holds. I@08:55:06.088 State 1: state invariant 21 holds. I@08:55:06.092 State 1: state invariant 22 holds. I@08:55:06.103 State 1: state invariant 23 holds. I@08:55:06.110 State 1: state invariant 24 holds. I@08:55:06.152 State 1: state invariant 25 holds. I@08:55:06.159 State 1: state invariant 26 holds. I@08:55:06.240 State 1: state invariant 27 holds. I@08:55:06.290 State 1: state invariant 28 holds. I@08:55:06.359 State 1: state invariant 29 holds. I@08:55:06.362 State 1: state invariant 30 holds. I@08:55:06.376 State 1: state invariant 31 holds. I@08:55:06.425 State 1: Checking 22 state invariants I@08:55:06.570 State 1: state invariant 0 holds. I@08:55:06.572 State 1: state invariant 1 holds. I@08:55:06.588 State 1: state invariant 5 holds. I@08:55:06.595 State 1: state invariant 6 holds. I@08:55:06.596 State 1: state invariant 9 holds. I@08:55:06.602 State 1: state invariant 10 holds. I@08:55:06.608 State 1: state invariant 11 holds. I@08:55:06.609 State 1: state invariant 12 holds. I@08:55:06.616 State 1: state invariant 13 holds. I@08:55:06.617 State 1: state invariant 14 holds. I@08:55:06.626 State 1: state invariant 15 holds. I@08:55:06.630 State 1: state invariant 16 holds. I@08:55:06.641 State 1: state invariant 17 holds. I@08:55:06.650 State 1: state invariant 19 holds. I@08:55:06.652 State 1: state invariant 21 holds. I@08:55:06.655 State 1: state invariant 22 holds. I@08:55:06.667 State 1: state invariant 23 holds. I@08:55:06.674 State 1: state invariant 24 holds. I@08:55:06.696 State 1: state invariant 25 holds. I@08:55:06.703 State 1: state invariant 26 holds. I@08:55:06.783 State 1: state invariant 27 holds. I@08:55:06.834 State 1: state invariant 28 holds. I@08:55:06.900 Step 1: Transition #12 is disabled I@08:55:06.935 State 1: Checking 21 state invariants I@08:55:06.981 State 1: state invariant 0 holds. I@08:55:06.982 State 1: state invariant 1 holds. I@08:55:06.999 State 1: state invariant 5 holds. I@08:55:07.005 State 1: state invariant 6 holds. I@08:55:07.007 State 1: state invariant 9 holds. I@08:55:07.013 State 1: state invariant 10 holds. I@08:55:07.020 State 1: state invariant 12 holds. I@08:55:07.026 State 1: state invariant 13 holds. I@08:55:07.027 State 1: state invariant 14 holds. I@08:55:07.040 State 1: state invariant 15 holds. I@08:55:07.056 State 1: state invariant 16 holds. I@08:55:07.065 State 1: state invariant 17 holds. I@08:55:07.085 State 1: state invariant 19 holds. I@08:55:07.088 State 1: state invariant 21 holds. I@08:55:07.090 State 1: state invariant 22 holds. I@08:55:07.102 State 1: state invariant 23 holds. I@08:55:07.110 State 1: state invariant 24 holds. I@08:55:07.160 State 1: state invariant 25 holds. I@08:55:07.168 State 1: state invariant 26 holds. I@08:55:07.309 State 1: state invariant 27 holds. I@08:55:07.389 State 1: state invariant 28 holds. I@08:55:07.520 Step 1: Transition #14 is disabled I@08:55:07.554 Step 1: Transition #15 is disabled I@08:55:07.609 State 1: Checking 14 state invariants I@08:55:07.670 State 1: state invariant 2 holds. I@08:55:07.670 State 1: state invariant 3 holds. I@08:55:07.673 State 1: state invariant 18 holds. I@08:55:07.687 State 1: state invariant 20 holds. I@08:55:07.691 State 1: state invariant 22 holds. I@08:55:07.705 State 1: state invariant 24 holds. I@08:55:07.738 State 1: state invariant 25 holds. I@08:55:07.744 State 1: state invariant 26 holds. I@08:55:07.833 State 1: state invariant 27 holds. I@08:55:07.871 State 1: state invariant 28 holds. I@08:55:07.915 State 1: state invariant 29 holds. I@08:55:07.919 State 1: state invariant 30 holds. I@08:55:07.930 State 1: state invariant 31 holds. I@08:55:07.944 State 1: state invariant 34 holds. I@08:55:07.946 State 1: Checking 21 state invariants I@08:55:08.016 State 1: state invariant 0 holds. I@08:55:08.018 State 1: state invariant 1 holds. I@08:55:08.036 State 1: state invariant 2 holds. I@08:55:08.037 State 1: state invariant 3 holds. I@08:55:08.038 State 1: state invariant 14 holds. I@08:55:08.049 State 1: state invariant 15 holds. I@08:55:08.055 State 1: state invariant 16 holds. I@08:55:08.061 State 1: state invariant 17 holds. I@08:55:08.076 State 1: state invariant 18 holds. I@08:55:08.090 State 1: state invariant 20 holds. I@08:55:08.091 State 1: state invariant 22 holds. I@08:55:08.096 State 1: state invariant 23 holds. I@08:55:08.104 State 1: state invariant 24 holds. I@08:55:08.146 State 1: state invariant 25 holds. I@08:55:08.152 State 1: state invariant 26 holds. I@08:55:08.294 State 1: state invariant 27 holds. I@08:55:08.352 State 1: state invariant 28 holds. I@08:55:08.437 State 1: state invariant 29 holds. I@08:55:08.441 State 1: state invariant 30 holds. I@08:55:08.454 State 1: state invariant 31 holds. I@08:55:08.468 State 1: state invariant 34 holds. I@08:55:08.469 Step 1: picking a transition out of 13 transition(s) I@08:55:08.471 The outcome is: NoError I@08:55:08.617 > [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'... PASS #0: SanyParser I@08:55:08.749 PASS #1: TypeCheckerSnowcat I@08:55:08.809 > Running Snowcat .::. I@08:55:08.809 > Your types are purrfect! I@08:55:10.272 > All expressions are typed I@08:55:10.273 PASS #2: ConfigurationPass I@08:55:10.273 > Set the initialization predicate to q::inductiveInv I@08:55:10.274 > Set the transition predicate to q::step I@08:55:10.274 > Set an invariant to q::inv I@08:55:10.274 PASS #3: DesugarerPass I@08:55:10.276 > Desugaring... I@08:55:10.276 PASS #4: InlinePass I@08:55:10.277 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@08:55:10.277 PASS #5: TemporalPass I@08:55:10.316 > Rewriting temporal operators... I@08:55:10.316 > No temporal property specified, nothing to encode I@08:55:10.316 PASS #6: InlinePass I@08:55:10.316 Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@08:55:10.316 PASS #7: PrimingPass I@08:55:10.332 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@08:55:10.332 PASS #8: VCGen I@08:55:10.333 > Producing verification conditions from the invariant q::inv I@08:55:10.333 > VCGen produced 5 verification condition(s) I@08:55:10.334 PASS #9: PreprocessingPass I@08:55:10.334 > Before preprocessing: unique renaming I@08:55:10.334 > Applying standard transformations: I@08:55:10.334 > PrimePropagation I@08:55:10.334 > Desugarer I@08:55:10.337 > UniqueRenamer I@08:55:10.342 > Normalizer I@08:55:10.358 > Keramelizer I@08:55:10.364 > After preprocessing: UniqueRenamer I@08:55:10.374 PASS #10: TransitionFinderPass I@08:55:10.393 > Found 1 initializing transitions I@08:55:10.395 > Found 18 transitions I@08:55:10.404 > No constant initializer I@08:55:10.404 > Applying unique renaming I@08:55:10.404 PASS #11: OptimizationPass I@08:55:10.429 > Applying optimizations: I@08:55:10.429 > ConstSimplifier I@08:55:10.429 > ExprOptimizer I@08:55:10.472 > SetMembershipSimplifier I@08:55:10.480 > ConstSimplifier I@08:55:10.485 PASS #12: AnalysisPass I@08:55:10.526 > Marking skolemizable existentials and sets to be expanded... I@08:55:10.526 > Skolemization I@08:55:10.526 > Expansion I@08:55:10.530 > Remove unused let-in defs I@08:55:10.536 > Running analyzers... I@08:55:10.540 > Introduced expression grades I@08:55:10.540 PASS #13: BoundedChecker I@08:55:10.540 State 0: Checking 5 state invariants I@08:55:10.921 State 0: state invariant 0 holds. I@08:55:10.922 State 0: state invariant 1 holds. I@08:55:10.923 State 0: state invariant 2 holds. I@08:55:10.924 State 0: state invariant 3 holds. I@08:55:10.928 State 0: state invariant 4 holds. I@08:55:10.984 Step 0: picking a transition out of 1 transition(s) I@08:55:10.987 The outcome is: NoError I@08:55:10.997 [ok] No violation found (20955ms). You may increase --max-steps. Use --verbosity to produce more (or less) output.