spec-protocol
checks.x86_64-linux.spec-protocol
· build #273
· raw
1tribuchet: building on jamie2> [1/3] Checking whether the inductive invariant 'indInv' holds in the initial state(s) defined by 'init'...3# Usage statistics is OFF. We care about your privacy.4# If you want to help our project, consider enabling statistics with config --enable-stats=true.56Output directory: /build/_apalache-out/server/2026-08-25T09-12-55_40339461238005006367# APALACHE version: 0.56.1 | build: 70cdaf4 I@09:12:55.6048Starting checker server on port 8822... I@09:12:55.6139The Apalache server is running on port 8822. Press Ctrl-C to stop.10Failed to find a usable hardware address from the network interfaces; using random bytes: 23:92:16:4e:ef:62:66:8b W@09:12:56.28811Aug 25, 2026 9:12:59 AM com.google.protobuf.GeneratedMessage warnPre22Gencode12WARNING: Vulnerable protobuf generated type in use: io.grpc.reflection.v1alpha.ServerReflectionRequest13As 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-j3g214PASS #0: SanyParser I@09:12:59.51515PASS #1: TypeCheckerSnowcat I@09:13:00.13716 > Running Snowcat .::. I@09:13:00.13717 > Your types are purrfect! I@09:13:02.04118 > All expressions are typed I@09:13:02.04219PASS #2: ConfigurationPass I@09:13:02.04320 > Set the initialization predicate to q::init I@09:13:02.04821 > Set the transition predicate to q::step I@09:13:02.04922 > Set an invariant to q::inductiveInv I@09:13:02.04923PASS #3: DesugarerPass I@09:13:02.05624 > Desugaring... I@09:13:02.05625PASS #4: InlinePass I@09:13:02.07126Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@09:13:02.07227PASS #5: TemporalPass I@09:13:02.17528 > Rewriting temporal operators... I@09:13:02.17529 > No temporal property specified, nothing to encode I@09:13:02.17530PASS #6: InlinePass I@09:13:02.17531Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@09:13:02.17532PASS #7: PrimingPass I@09:13:02.20433 > Introducing q::initPrimed for q::init' I@09:13:02.20734PASS #8: VCGen I@09:13:02.20935 > Producing verification conditions from the invariant q::inductiveInv I@09:13:02.20936 > VCGen produced 35 verification condition(s) I@09:13:02.21837PASS #9: PreprocessingPass I@09:13:02.22138 > Before preprocessing: unique renaming I@09:13:02.22139 > Applying standard transformations: I@09:13:02.22940 > PrimePropagation I@09:13:02.22941 > Desugarer I@09:13:02.23542 > UniqueRenamer I@09:13:02.24543 > Normalizer I@09:13:02.26544 > Keramelizer I@09:13:02.28345 > After preprocessing: UniqueRenamer I@09:13:02.30746PASS #10: TransitionFinderPass I@09:13:02.34547 > Found 1 initializing transitions I@09:13:02.35848 > Found 18 transitions I@09:13:02.38649 > No constant initializer I@09:13:02.38650 > Applying unique renaming I@09:13:02.38751PASS #11: OptimizationPass I@09:13:02.41552 > Applying optimizations: I@09:13:02.42353 > ConstSimplifier I@09:13:02.42454 > ExprOptimizer I@09:13:02.47755 > SetMembershipSimplifier I@09:13:02.50156 > ConstSimplifier I@09:13:02.50957PASS #12: AnalysisPass I@09:13:02.55558 > Marking skolemizable existentials and sets to be expanded... I@09:13:02.55859 > Skolemization I@09:13:02.55860 > Expansion I@09:13:02.56461 > Remove unused let-in defs I@09:13:02.58062 > Running analyzers... I@09:13:02.59163 > Introduced expression grades I@09:13:02.60264PASS #13: BoundedChecker I@09:13:02.60265State 0: Checking 35 state invariants I@09:13:03.10666State 0: state invariant 0 holds. I@09:13:03.10967State 0: state invariant 1 holds. I@09:13:03.15068State 0: state invariant 2 holds. I@09:13:03.15169State 0: state invariant 3 holds. I@09:13:03.15270State 0: state invariant 4 holds. I@09:13:03.15471State 0: state invariant 5 holds. I@09:13:03.16172State 0: state invariant 6 holds. I@09:13:03.16273State 0: state invariant 7 holds. I@09:13:03.16274State 0: state invariant 8 holds. I@09:13:03.16375State 0: state invariant 9 holds. I@09:13:03.17276State 0: state invariant 10 holds. I@09:13:03.17377State 0: state invariant 11 holds. I@09:13:03.17478State 0: state invariant 12 holds. I@09:13:03.18279State 0: state invariant 13 holds. I@09:13:03.18380State 0: state invariant 14 holds. I@09:13:03.18681State 0: state invariant 15 holds. I@09:13:03.19282State 0: state invariant 16 holds. I@09:13:03.19983State 0: state invariant 17 holds. I@09:13:03.20484State 0: state invariant 18 holds. I@09:13:03.20985State 0: state invariant 19 holds. I@09:13:03.21186State 0: state invariant 20 holds. I@09:13:03.21187State 0: state invariant 21 holds. I@09:13:03.21888State 0: state invariant 22 holds. I@09:13:03.22889State 0: state invariant 23 holds. I@09:13:03.23690State 0: state invariant 24 holds. I@09:13:03.25891State 0: state invariant 25 holds. I@09:13:03.26492State 0: state invariant 26 holds. I@09:13:03.28393State 0: state invariant 27 holds. I@09:13:03.30794State 0: state invariant 28 holds. I@09:13:03.33395State 0: state invariant 29 holds. I@09:13:03.33496State 0: state invariant 30 holds. I@09:13:03.34497State 0: state invariant 31 holds. I@09:13:03.35498State 0: state invariant 32 holds. I@09:13:03.35599State 0: state invariant 33 holds. I@09:13:03.355100State 0: state invariant 34 holds. I@09:13:03.356101Step 0: picking a transition out of 1 transition(s) I@09:13:03.356102The outcome is: NoError I@09:13:03.365103> [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'...104PASS #0: SanyParser I@09:13:03.686105PASS #1: TypeCheckerSnowcat I@09:13:03.789106 > Running Snowcat .::. I@09:13:03.789107 > Your types are purrfect! I@09:13:05.561108 > All expressions are typed I@09:13:05.562109PASS #2: ConfigurationPass I@09:13:05.562110 > Set the initialization predicate to q::inductiveInv I@09:13:05.563111 > Set the transition predicate to q::step I@09:13:05.563112 > Set an invariant to q::inductiveInv I@09:13:05.563113PASS #3: DesugarerPass I@09:13:05.565114 > Desugaring... I@09:13:05.565115PASS #4: InlinePass I@09:13:05.567116Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@09:13:05.567117PASS #5: TemporalPass I@09:13:05.594118 > Rewriting temporal operators... I@09:13:05.594119 > No temporal property specified, nothing to encode I@09:13:05.594120PASS #6: InlinePass I@09:13:05.594121Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@09:13:05.594122PASS #7: PrimingPass I@09:13:05.602123 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@09:13:05.603124PASS #8: VCGen I@09:13:05.604125 > Producing verification conditions from the invariant q::inductiveInv I@09:13:05.604126 > VCGen produced 35 verification condition(s) I@09:13:05.605127PASS #9: PreprocessingPass I@09:13:05.606128 > Before preprocessing: unique renaming I@09:13:05.606129 > Applying standard transformations: I@09:13:05.606130 > PrimePropagation I@09:13:05.606131 > Desugarer I@09:13:05.608132 > UniqueRenamer I@09:13:05.614133 > Normalizer I@09:13:05.623134 > Keramelizer I@09:13:05.637135 > After preprocessing: UniqueRenamer I@09:13:05.646136PASS #10: TransitionFinderPass I@09:13:05.658137 > Found 1 initializing transitions I@09:13:05.661138 > Found 18 transitions I@09:13:05.670139 > No constant initializer I@09:13:05.670140 > Applying unique renaming I@09:13:05.670141PASS #11: OptimizationPass I@09:13:05.688142 > Applying optimizations: I@09:13:05.688143 > ConstSimplifier I@09:13:05.688144 > ExprOptimizer I@09:13:05.746145 > SetMembershipSimplifier I@09:13:05.758146 > ConstSimplifier I@09:13:05.762147PASS #12: AnalysisPass I@09:13:05.813148 > Marking skolemizable existentials and sets to be expanded... I@09:13:05.814149 > Skolemization I@09:13:05.814150 > Expansion I@09:13:05.817151 > Remove unused let-in defs I@09:13:05.828152 > Running analyzers... I@09:13:05.831153 > Introduced expression grades I@09:13:05.833154PASS #13: BoundedChecker I@09:13:05.833155State 0: Checking 35 state invariants I@09:13:06.335156State 0: state invariant 0 holds. I@09:13:06.336157State 0: state invariant 1 holds. I@09:13:06.355158State 0: state invariant 2 holds. I@09:13:06.357159State 0: state invariant 3 holds. I@09:13:06.358160State 0: state invariant 4 holds. I@09:13:06.359161State 0: state invariant 5 holds. I@09:13:06.362162State 0: state invariant 6 holds. I@09:13:06.364163State 0: state invariant 7 holds. I@09:13:06.365164State 0: state invariant 8 holds. I@09:13:06.367165State 0: state invariant 9 holds. I@09:13:06.374166State 0: state invariant 10 holds. I@09:13:06.375167State 0: state invariant 11 holds. I@09:13:06.376168State 0: state invariant 12 holds. I@09:13:06.382169State 0: state invariant 13 holds. I@09:13:06.383170State 0: state invariant 14 holds. I@09:13:06.388171State 0: state invariant 15 holds. I@09:13:06.394172State 0: state invariant 16 holds. I@09:13:06.406173State 0: state invariant 17 holds. I@09:13:06.416174State 0: state invariant 18 holds. I@09:13:06.425175State 0: state invariant 19 holds. I@09:13:06.426176State 0: state invariant 20 holds. I@09:13:06.426177State 0: state invariant 21 holds. I@09:13:06.428178State 0: state invariant 22 holds. I@09:13:06.432179State 0: state invariant 23 holds. I@09:13:06.440180State 0: state invariant 24 holds. I@09:13:06.494181State 0: state invariant 25 holds. I@09:13:06.501182State 0: state invariant 26 holds. I@09:13:06.600183State 0: state invariant 27 holds. I@09:13:06.666184State 0: state invariant 28 holds. I@09:13:06.787185State 0: state invariant 29 holds. I@09:13:06.790186State 0: state invariant 30 holds. I@09:13:06.803187State 0: state invariant 31 holds. I@09:13:06.818188State 0: state invariant 32 holds. I@09:13:06.819189State 0: state invariant 33 holds. I@09:13:06.820190State 0: state invariant 34 holds. I@09:13:06.821191Step 0: picking a transition out of 1 transition(s) I@09:13:06.822192State 1: Checking 4 state invariants I@09:13:06.834193State 1: state invariant 8 holds. I@09:13:06.835194State 1: state invariant 25 holds. I@09:13:06.840195State 1: state invariant 26 holds. I@09:13:06.949196State 1: state invariant 27 holds. I@09:13:07.018197State 1: Checking 15 state invariants I@09:13:07.034198State 1: state invariant 0 holds. I@09:13:07.035199State 1: state invariant 1 holds. I@09:13:07.052200State 1: state invariant 12 holds. I@09:13:07.060201State 1: state invariant 14 holds. I@09:13:07.068202State 1: state invariant 15 holds. I@09:13:07.073203State 1: state invariant 16 holds. I@09:13:07.080204State 1: state invariant 17 holds. I@09:13:07.091205State 1: state invariant 22 holds. I@09:13:07.099206State 1: state invariant 24 holds. I@09:13:07.148207State 1: state invariant 25 holds. I@09:13:07.155208State 1: state invariant 26 holds. I@09:13:07.239209State 1: state invariant 27 holds. I@09:13:07.309210State 1: state invariant 28 holds. I@09:13:07.389211State 1: state invariant 33 holds. I@09:13:07.392212State 1: state invariant 34 holds. I@09:13:07.393213State 1: Checking 18 state invariants I@09:13:07.532214State 1: state invariant 5 holds. I@09:13:07.536215State 1: state invariant 6 holds. I@09:13:07.538216State 1: state invariant 7 holds. I@09:13:07.539217State 1: state invariant 9 holds. I@09:13:07.545218State 1: state invariant 10 holds. I@09:13:07.546219State 1: state invariant 13 holds. I@09:13:07.547220State 1: state invariant 18 holds. I@09:13:07.557221State 1: state invariant 19 holds. I@09:13:07.558222State 1: state invariant 21 holds. I@09:13:07.560223State 1: state invariant 22 holds. I@09:13:07.569224State 1: state invariant 24 holds. I@09:13:07.606225State 1: state invariant 25 holds. I@09:13:07.612226State 1: state invariant 26 holds. I@09:13:07.659227State 1: state invariant 27 holds. I@09:13:07.693228State 1: state invariant 28 holds. I@09:13:07.756229State 1: state invariant 29 holds. I@09:13:07.759230State 1: state invariant 30 holds. I@09:13:07.776231State 1: state invariant 31 holds. I@09:13:07.816232State 1: Checking 14 state invariants I@09:13:07.928233State 1: state invariant 5 holds. I@09:13:07.932234State 1: state invariant 6 holds. I@09:13:07.934235State 1: state invariant 7 holds. I@09:13:07.936236State 1: state invariant 9 holds. I@09:13:07.942237State 1: state invariant 10 holds. I@09:13:07.944238State 1: state invariant 13 holds. I@09:13:07.945239State 1: state invariant 19 holds. I@09:13:07.947240State 1: state invariant 21 holds. I@09:13:07.949241State 1: state invariant 22 holds. I@09:13:07.954242State 1: state invariant 24 holds. I@09:13:07.974243State 1: state invariant 25 holds. I@09:13:07.980244State 1: state invariant 26 holds. I@09:13:08.114245State 1: state invariant 27 holds. I@09:13:08.146246State 1: state invariant 28 holds. I@09:13:08.188247State 1: Checking 26 state invariants I@09:13:08.285248State 1: state invariant 0 holds. I@09:13:08.286249State 1: state invariant 1 holds. I@09:13:08.304250State 1: state invariant 5 holds. I@09:13:08.309251State 1: state invariant 6 holds. I@09:13:08.310252State 1: state invariant 7 holds. I@09:13:08.311253State 1: state invariant 9 holds. I@09:13:08.318254State 1: state invariant 10 holds. I@09:13:08.333255State 1: state invariant 12 holds. I@09:13:08.339256State 1: state invariant 13 holds. I@09:13:08.340257State 1: state invariant 14 holds. I@09:13:08.346258State 1: state invariant 15 holds. I@09:13:08.361259State 1: state invariant 16 holds. I@09:13:08.367260State 1: state invariant 17 holds. I@09:13:08.381261State 1: state invariant 18 holds. I@09:13:08.396262State 1: state invariant 19 holds. I@09:13:08.398263State 1: state invariant 21 holds. I@09:13:08.400264State 1: state invariant 22 holds. I@09:13:08.417265State 1: state invariant 23 holds. I@09:13:08.424266State 1: state invariant 24 holds. I@09:13:08.484267State 1: state invariant 25 holds. I@09:13:08.491268State 1: state invariant 26 holds. I@09:13:08.590269State 1: state invariant 27 holds. I@09:13:08.664270State 1: state invariant 28 holds. I@09:13:08.773271State 1: state invariant 29 holds. I@09:13:08.776272State 1: state invariant 30 holds. I@09:13:08.792273State 1: state invariant 31 holds. I@09:13:08.844274State 1: Checking 22 state invariants I@09:13:08.937275State 1: state invariant 0 holds. I@09:13:08.939276State 1: state invariant 1 holds. I@09:13:08.958277State 1: state invariant 5 holds. I@09:13:08.963278State 1: state invariant 6 holds. I@09:13:08.965279State 1: state invariant 7 holds. I@09:13:08.966280State 1: state invariant 9 holds. I@09:13:08.974281State 1: state invariant 10 holds. I@09:13:08.978282State 1: state invariant 12 holds. I@09:13:08.983283State 1: state invariant 13 holds. I@09:13:08.985284State 1: state invariant 14 holds. I@09:13:08.991285State 1: state invariant 15 holds. I@09:13:08.997286State 1: state invariant 16 holds. I@09:13:09.003287State 1: state invariant 17 holds. I@09:13:09.012288State 1: state invariant 19 holds. I@09:13:09.014289State 1: state invariant 21 holds. I@09:13:09.017290State 1: state invariant 22 holds. I@09:13:09.029291State 1: state invariant 23 holds. I@09:13:09.036292State 1: state invariant 24 holds. I@09:13:09.092293State 1: state invariant 25 holds. I@09:13:09.099294State 1: state invariant 26 holds. I@09:13:09.214295State 1: state invariant 27 holds. I@09:13:09.282296State 1: state invariant 28 holds. I@09:13:09.369297Step 1: Transition #6 is disabled I@09:13:09.404298Step 1: Transition #7 is disabled I@09:13:09.431299State 1: Checking 27 state invariants I@09:13:09.538300State 1: state invariant 0 holds. I@09:13:09.539301State 1: state invariant 1 holds. I@09:13:09.552302State 1: state invariant 5 holds. I@09:13:09.559303State 1: state invariant 6 holds. I@09:13:09.560304State 1: state invariant 8 holds. I@09:13:09.561305State 1: state invariant 9 holds. I@09:13:09.566306State 1: state invariant 10 holds. I@09:13:09.574307State 1: state invariant 11 holds. I@09:13:09.575308State 1: state invariant 12 holds. I@09:13:09.580309State 1: state invariant 13 holds. I@09:13:09.581310State 1: state invariant 14 holds. I@09:13:09.586311State 1: state invariant 15 holds. I@09:13:09.594312State 1: state invariant 16 holds. I@09:13:09.601313State 1: state invariant 17 holds. I@09:13:09.608314State 1: state invariant 18 holds. I@09:13:09.624315State 1: state invariant 19 holds. I@09:13:09.626316State 1: state invariant 21 holds. I@09:13:09.629317State 1: state invariant 22 holds. I@09:13:09.641318State 1: state invariant 23 holds. I@09:13:09.648319State 1: state invariant 24 holds. I@09:13:09.710320State 1: state invariant 25 holds. I@09:13:09.716321State 1: state invariant 26 holds. I@09:13:09.805322State 1: state invariant 27 holds. I@09:13:09.863323State 1: state invariant 28 holds. I@09:13:09.959324State 1: state invariant 29 holds. I@09:13:09.962325State 1: state invariant 30 holds. I@09:13:09.976326State 1: state invariant 31 holds. I@09:13:10.022327State 1: Checking 23 state invariants I@09:13:10.103328State 1: state invariant 0 holds. I@09:13:10.104329State 1: state invariant 1 holds. I@09:13:10.118330State 1: state invariant 5 holds. I@09:13:10.125331State 1: state invariant 6 holds. I@09:13:10.126332State 1: state invariant 8 holds. I@09:13:10.127333State 1: state invariant 9 holds. I@09:13:10.133334State 1: state invariant 10 holds. I@09:13:10.140335State 1: state invariant 11 holds. I@09:13:10.142336State 1: state invariant 12 holds. I@09:13:10.146337State 1: state invariant 13 holds. I@09:13:10.147338State 1: state invariant 14 holds. I@09:13:10.154339State 1: state invariant 15 holds. I@09:13:10.162340State 1: state invariant 16 holds. I@09:13:10.169341State 1: state invariant 17 holds. I@09:13:10.177342State 1: state invariant 19 holds. I@09:13:10.179343State 1: state invariant 21 holds. I@09:13:10.181344State 1: state invariant 22 holds. I@09:13:10.187345State 1: state invariant 23 holds. I@09:13:10.194346State 1: state invariant 24 holds. I@09:13:10.223347State 1: state invariant 25 holds. I@09:13:10.228348State 1: state invariant 26 holds. I@09:13:10.325349State 1: state invariant 27 holds. I@09:13:10.394350State 1: state invariant 28 holds. I@09:13:10.474351State 1: Checking 26 state invariants I@09:13:10.638352State 1: state invariant 0 holds. I@09:13:10.639353State 1: state invariant 1 holds. I@09:13:10.652354State 1: state invariant 5 holds. I@09:13:10.659355State 1: state invariant 6 holds. I@09:13:10.660356State 1: state invariant 9 holds. I@09:13:10.666357State 1: state invariant 10 holds. I@09:13:10.669358State 1: state invariant 11 holds. I@09:13:10.670359State 1: state invariant 12 holds. I@09:13:10.675360State 1: state invariant 13 holds. I@09:13:10.676361State 1: state invariant 14 holds. I@09:13:10.682362State 1: state invariant 15 holds. I@09:13:10.685363State 1: state invariant 16 holds. I@09:13:10.690364State 1: state invariant 17 holds. I@09:13:10.698365State 1: state invariant 18 holds. I@09:13:10.710366State 1: state invariant 19 holds. I@09:13:10.712367State 1: state invariant 21 holds. I@09:13:10.714368State 1: state invariant 22 holds. I@09:13:10.724369State 1: state invariant 23 holds. I@09:13:10.731370State 1: state invariant 24 holds. I@09:13:10.769371State 1: state invariant 25 holds. I@09:13:10.775372State 1: state invariant 26 holds. I@09:13:10.842373State 1: state invariant 27 holds. I@09:13:10.886374State 1: state invariant 28 holds. I@09:13:10.957375State 1: state invariant 29 holds. I@09:13:10.969376State 1: state invariant 30 holds. I@09:13:10.981377State 1: state invariant 31 holds. I@09:13:11.024378State 1: Checking 22 state invariants I@09:13:11.170379State 1: state invariant 0 holds. I@09:13:11.172380State 1: state invariant 1 holds. I@09:13:11.188381State 1: state invariant 5 holds. I@09:13:11.197382State 1: state invariant 6 holds. I@09:13:11.198383State 1: state invariant 9 holds. I@09:13:11.204384State 1: state invariant 10 holds. I@09:13:11.206385State 1: state invariant 11 holds. I@09:13:11.207386State 1: state invariant 12 holds. I@09:13:11.213387State 1: state invariant 13 holds. I@09:13:11.214388State 1: state invariant 14 holds. I@09:13:11.223389State 1: state invariant 15 holds. I@09:13:11.230390State 1: state invariant 16 holds. I@09:13:11.242391State 1: state invariant 17 holds. I@09:13:11.255392State 1: state invariant 19 holds. I@09:13:11.257393State 1: state invariant 21 holds. I@09:13:11.261394State 1: state invariant 22 holds. I@09:13:11.274395State 1: state invariant 23 holds. I@09:13:11.281396State 1: state invariant 24 holds. I@09:13:11.310397State 1: state invariant 25 holds. I@09:13:11.316398State 1: state invariant 26 holds. I@09:13:11.420399State 1: state invariant 27 holds. I@09:13:11.479400State 1: state invariant 28 holds. I@09:13:11.547401Step 1: Transition #12 is disabled I@09:13:11.581402State 1: Checking 21 state invariants I@09:13:11.671403State 1: state invariant 0 holds. I@09:13:11.672404State 1: state invariant 1 holds. I@09:13:11.689405State 1: state invariant 5 holds. I@09:13:11.697406State 1: state invariant 6 holds. I@09:13:11.698407State 1: state invariant 9 holds. I@09:13:11.704408State 1: state invariant 10 holds. I@09:13:11.710409State 1: state invariant 12 holds. I@09:13:11.717410State 1: state invariant 13 holds. I@09:13:11.719411State 1: state invariant 14 holds. I@09:13:11.725412State 1: state invariant 15 holds. I@09:13:11.736413State 1: state invariant 16 holds. I@09:13:11.753414State 1: state invariant 17 holds. I@09:13:11.769415State 1: state invariant 19 holds. I@09:13:11.771416State 1: state invariant 21 holds. I@09:13:11.773417State 1: state invariant 22 holds. I@09:13:11.782418State 1: state invariant 23 holds. I@09:13:11.789419State 1: state invariant 24 holds. I@09:13:11.830420State 1: state invariant 25 holds. I@09:13:11.837421State 1: state invariant 26 holds. I@09:13:11.960422State 1: state invariant 27 holds. I@09:13:12.049423State 1: state invariant 28 holds. I@09:13:12.162424Step 1: Transition #14 is disabled I@09:13:12.196425Step 1: Transition #15 is disabled I@09:13:12.245426State 1: Checking 14 state invariants I@09:13:12.301427State 1: state invariant 2 holds. I@09:13:12.302428State 1: state invariant 3 holds. I@09:13:12.304429State 1: state invariant 18 holds. I@09:13:12.311430State 1: state invariant 20 holds. I@09:13:12.312431State 1: state invariant 22 holds. I@09:13:12.317432State 1: state invariant 24 holds. I@09:13:12.337433State 1: state invariant 25 holds. I@09:13:12.343434State 1: state invariant 26 holds. I@09:13:12.393435State 1: state invariant 27 holds. I@09:13:12.422436State 1: state invariant 28 holds. I@09:13:12.462437State 1: state invariant 29 holds. I@09:13:12.467438State 1: state invariant 30 holds. I@09:13:12.479439State 1: state invariant 31 holds. I@09:13:12.492440State 1: state invariant 34 holds. I@09:13:12.494441State 1: Checking 21 state invariants I@09:13:12.550442State 1: state invariant 0 holds. I@09:13:12.551443State 1: state invariant 1 holds. I@09:13:12.572444State 1: state invariant 2 holds. I@09:13:12.574445State 1: state invariant 3 holds. I@09:13:12.575446State 1: state invariant 14 holds. I@09:13:12.582447State 1: state invariant 15 holds. I@09:13:12.588448State 1: state invariant 16 holds. I@09:13:12.597449State 1: state invariant 17 holds. I@09:13:12.609450State 1: state invariant 18 holds. I@09:13:12.623451State 1: state invariant 20 holds. I@09:13:12.624452State 1: state invariant 22 holds. I@09:13:12.628453State 1: state invariant 23 holds. I@09:13:12.637454State 1: state invariant 24 holds. I@09:13:12.699455State 1: state invariant 25 holds. I@09:13:12.707456State 1: state invariant 26 holds. I@09:13:12.882457State 1: state invariant 27 holds. I@09:13:12.945458State 1: state invariant 28 holds. I@09:13:13.039459State 1: state invariant 29 holds. I@09:13:13.043460State 1: state invariant 30 holds. I@09:13:13.055461State 1: state invariant 31 holds. I@09:13:13.069462State 1: state invariant 34 holds. I@09:13:13.071463Step 1: picking a transition out of 13 transition(s) I@09:13:13.073464The outcome is: NoError I@09:13:13.235465> [3/3] Checking whether the inductive invariant 'indInv' implies 'inv'...466PASS #0: SanyParser I@09:13:13.404467PASS #1: TypeCheckerSnowcat I@09:13:13.477468 > Running Snowcat .::. I@09:13:13.477469 > Your types are purrfect! I@09:13:14.875470 > All expressions are typed I@09:13:14.876471PASS #2: ConfigurationPass I@09:13:14.876472 > Set the initialization predicate to q::inductiveInv I@09:13:14.877473 > Set the transition predicate to q::step I@09:13:14.877474 > Set an invariant to q::inv I@09:13:14.877475PASS #3: DesugarerPass I@09:13:14.878476 > Desugaring... I@09:13:14.878477PASS #4: InlinePass I@09:13:14.879478Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@09:13:14.880479PASS #5: TemporalPass I@09:13:14.901480 > Rewriting temporal operators... I@09:13:14.902481 > No temporal property specified, nothing to encode I@09:13:14.902482PASS #6: InlinePass I@09:13:14.902483Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::inv, q::step I@09:13:14.902484PASS #7: PrimingPass I@09:13:14.910485 > Introducing q::inductiveInvPrimed for q::inductiveInv' I@09:13:14.910486PASS #8: VCGen I@09:13:14.911487 > Producing verification conditions from the invariant q::inv I@09:13:14.911488 > VCGen produced 5 verification condition(s) I@09:13:14.912489PASS #9: PreprocessingPass I@09:13:14.912490 > Before preprocessing: unique renaming I@09:13:14.912491 > Applying standard transformations: I@09:13:14.912492 > PrimePropagation I@09:13:14.912493 > Desugarer I@09:13:14.914494 > UniqueRenamer I@09:13:14.917495 > Normalizer I@09:13:14.925496 > Keramelizer I@09:13:14.929497 > After preprocessing: UniqueRenamer I@09:13:14.936498PASS #10: TransitionFinderPass I@09:13:14.945499 > Found 1 initializing transitions I@09:13:14.946500 > Found 18 transitions I@09:13:14.952501 > No constant initializer I@09:13:14.952502 > Applying unique renaming I@09:13:14.953503PASS #11: OptimizationPass I@09:13:14.964504 > Applying optimizations: I@09:13:14.964505 > ConstSimplifier I@09:13:14.964506 > ExprOptimizer I@09:13:15.006507 > SetMembershipSimplifier I@09:13:15.012508 > ConstSimplifier I@09:13:15.014509PASS #12: AnalysisPass I@09:13:15.055510 > Marking skolemizable existentials and sets to be expanded... I@09:13:15.055511 > Skolemization I@09:13:15.055512 > Expansion I@09:13:15.057513 > Remove unused let-in defs I@09:13:15.062514 > Running analyzers... I@09:13:15.064515 > Introduced expression grades I@09:13:15.065516PASS #13: BoundedChecker I@09:13:15.065517State 0: Checking 5 state invariants I@09:13:15.408518State 0: state invariant 0 holds. I@09:13:15.409519State 0: state invariant 1 holds. I@09:13:15.410520State 0: state invariant 2 holds. I@09:13:15.411521State 0: state invariant 3 holds. I@09:13:15.415522State 0: state invariant 4 holds. I@09:13:15.469523Step 0: picking a transition out of 1 transition(s) I@09:13:15.471524The outcome is: NoError I@09:13:15.482525[ok] No violation found (20546ms).526You may increase --max-steps.527Use --verbosity to produce more (or less) output.