apalache
apalache copied to clipboard
Published
20 hours ago •
apalache-mc
apalache-mc
Damanged arena with `simulate`
Description
Running apalache-mc simulate on MC_LamportMutexTyped.tla results in an uncaught exception
internal error: SMT 0: Declaring cell 5, while cell 21799 has been already declared. Damaged arena?
on the third symbolic run.
Input specification
test/tla/MC_LamportMutexTyped.tla
The command line parameters used to run the tool
--features=rows --length=6 --inv=Mutex --discard-disabled=false --no-deadlock
Log files
11:13:02.228 [main] INFO a.f.a.t.Tool\$ - # APALACHE version: v0.27.0-2-g09ff5045d | build: v0.27.0-2-g09ff5045d
11:13:02.229 [main] INFO a.f.a.t.t.o.SimulateCmd - Tuning: search.simulation=true:search.simulation.maxRun=100:search.simulation.saveRuns=false
11:13:02.230 [main] INFO a.f.a.t.t.o.SimulateCmd - Checker options: simulate --features=rows --length=6 --inv=Mutex --discard-disabled=false --no-deadlock test/tla/MC_LamportMutexTyped.tla
11:13:02.231 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
11:13:02.426 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
11:13:02.427 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
11:13:02.427 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > Running Snowcat .::.
11:13:02.460 [main] WARN a.f.a.t.t.TypeCheckerTool - Operator network: Deprecated syntax in type alias MESSAGE. Use camelCase of Type System 1.2.
11:13:02.734 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > Your types are purrfect!
11:13:02.734 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > All expressions are typed
11:13:02.734 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
11:13:02.734 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass
11:13:02.738 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Command line option --init is not set. Using Init
11:13:02.738 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Command line option --next is not set. Using Next
11:13:02.738 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the initialization predicate to Init
11:13:02.738 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the transition predicate to Next
11:13:02.738 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set an invariant to Mutex
11:13:02.741 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK]
11:13:02.741 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass
11:13:02.741 [main] INFO a.f.a.t.p.p.DesugarerPassImpl - > Desugaring...
11:13:02.860 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK]
11:13:02.860 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass
11:13:02.860 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Mutex, Next
11:13:02.896 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass [OK]
11:13:02.896 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #5: TemporalPass
11:13:02.896 [main] INFO a.f.a.t.p.p.TemporalPassImpl - > Rewriting temporal operators...
11:13:02.896 [main] INFO a.f.a.t.p.p.TemporalPassImpl - > No temporal property specified, nothing to encode
11:13:02.896 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: TemporalPass [OK]
11:13:02.896 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #6: InlinePass
11:13:02.896 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Mutex, Next
11:13:02.903 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: InlinePass [OK]
11:13:02.903 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #7: PrimingPass
11:13:02.905 [main] INFO a.f.a.t.a.p.PrimingPassImpl - > Introducing InitPrimed for Init'
11:13:02.907 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: PrimingPass [OK]
11:13:02.907 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #8: VCGen
11:13:02.907 [main] INFO a.f.a.t.b.p.VCGenPassImpl - > Producing verification conditions from the invariant Mutex
11:13:02.910 [main] INFO a.f.a.t.b.VCGenerator - > VCGen produced 1 verification condition(s)
11:13:02.910 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: VCGen [OK]
11:13:02.910 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #9: PreprocessingPass
11:13:02.910 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Before preprocessing: unique renaming
11:13:02.914 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Applying standard transformations:
11:13:02.914 [main] INFO a.f.a.t.p.p.PreproPassImpl - > PrimePropagation
11:13:02.916 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Desugarer
11:13:02.919 [main] INFO a.f.a.t.p.p.PreproPassImpl - > UniqueRenamer
11:13:02.923 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Normalizer
11:13:02.926 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Keramelizer
11:13:02.933 [main] INFO a.f.a.t.p.p.PreproPassImpl - > After preprocessing: UniqueRenamer
11:13:02.937 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: PreprocessingPass [OK]
11:13:02.937 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #10: TransitionFinderPass
11:13:02.959 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Found 1 initializing transitions
11:13:02.970 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Found 6 transitions
11:13:02.971 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > No constant initializer
11:13:02.971 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Applying unique renaming
11:13:02.977 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: TransitionFinderPass [OK]
11:13:02.977 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #11: OptimizationPass
11:13:02.981 [main] INFO a.f.a.t.p.p.OptPassImpl - > Applying optimizations:
11:13:02.981 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier
11:13:02.985 [main] INFO a.f.a.t.p.p.OptPassImpl - > ExprOptimizer
11:13:02.988 [main] INFO a.f.a.t.p.p.OptPassImpl - > SetMembershipSimplifier
11:13:02.989 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier
11:13:02.992 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: OptimizationPass [OK]
11:13:02.992 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #12: AnalysisPass
11:13:02.995 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Marking skolemizable existentials and sets to be expanded...
11:13:02.995 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Skolemization
11:13:02.995 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Expansion
11:13:02.997 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Remove unused let-in defs
11:13:03.000 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Running analyzers...
11:13:03.001 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Introduced expression grades
11:13:03.002 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #12: AnalysisPass [OK]
11:13:03.002 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #13: BoundedChecker
11:13:03.382 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
11:13:03.382 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.414 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
11:13:03.417 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #1
11:13:03.417 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.464 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
11:13:03.464 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.538 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #4
11:13:03.538 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.582 [main] INFO a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
11:13:03.582 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 0
11:13:03.586 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #3
11:13:03.586 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.611 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #5
11:13:03.611 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.648 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #2
11:13:03.648 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.669 [main] INFO a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
11:13:03.669 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 0
11:13:03.671 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 1: picking a transition out of 6 transition(s)
11:13:03.701 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #5
11:13:03.701 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.758 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #3
11:13:03.759 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.791 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #4
11:13:03.791 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.839 [main] INFO a.f.a.t.b.SeqModelChecker - State 2: Checking 1 state invariants
11:13:03.840 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 0
11:13:03.843 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #0
11:13:03.843 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.896 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #2
11:13:03.896 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.940 [main] INFO a.f.a.t.b.SeqModelChecker - State 2: Checking 1 state invariants
11:13:03.941 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 0
11:13:03.954 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #1
11:13:03.954 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:03.982 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 2: picking a transition out of 6 transition(s)
11:13:04.007 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #5
11:13:04.007 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.067 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #0
11:13:04.067 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.125 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #3
11:13:04.125 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.158 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #1
11:13:04.158 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.188 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #2
11:13:04.188 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.232 [main] INFO a.f.a.t.b.SeqModelChecker - State 3: Checking 1 state invariants
11:13:04.232 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 3: Checking state invariant 0
11:13:04.236 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #4
11:13:04.236 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.276 [main] INFO a.f.a.t.b.SeqModelChecker - State 3: Checking 1 state invariants
11:13:04.277 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 3: Checking state invariant 0
11:13:04.281 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 3: picking a transition out of 6 transition(s)
11:13:04.308 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #0
11:13:04.308 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.370 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #5
11:13:04.370 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.433 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #2
11:13:04.433 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.487 [main] INFO a.f.a.t.b.SeqModelChecker - State 4: Checking 1 state invariants
11:13:04.487 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 4: Checking state invariant 0
11:13:04.491 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #4
11:13:04.491 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.529 [main] INFO a.f.a.t.b.SeqModelChecker - State 4: Checking 1 state invariants
11:13:04.529 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 4: Checking state invariant 0
11:13:04.547 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #1
11:13:04.547 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.584 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #3
11:13:04.584 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.629 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 4: picking a transition out of 6 transition(s)
11:13:04.661 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #1
11:13:04.662 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.709 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #0
11:13:04.709 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.777 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #4
11:13:04.778 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:04.874 [main] INFO a.f.a.t.b.SeqModelChecker - State 5: Checking 1 state invariants
11:13:04.875 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 5: Checking state invariant 0
11:13:05.113 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #3
11:13:05.113 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:05.153 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #2
11:13:05.154 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:05.212 [main] INFO a.f.a.t.b.SeqModelChecker - State 5: Checking 1 state invariants
11:13:05.212 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 5: Checking state invariant 0
11:13:05.307 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #5
11:13:05.308 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:05.373 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 5: picking a transition out of 6 transition(s)
11:13:05.408 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #4
11:13:05.408 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:05.449 [main] INFO a.f.a.t.b.SeqModelChecker - State 6: Checking 1 state invariants
11:13:05.449 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 6: Checking state invariant 0
11:13:06.763 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #2
11:13:06.763 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:06.830 [main] INFO a.f.a.t.b.SeqModelChecker - State 6: Checking 1 state invariants
11:13:06.830 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 6: Checking state invariant 0
11:13:06.984 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #0
11:13:06.984 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.063 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #5
11:13:07.063 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.152 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #3
11:13:07.152 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.207 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #1
11:13:07.208 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.264 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 6: picking a transition out of 6 transition(s)
11:13:07.332 [main] INFO a.f.a.t.b.SeqModelChecker - ----------------------------
11:13:07.332 [main] INFO a.f.a.t.b.SeqModelChecker - Symbolic runs left: 99
11:13:07.332 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
11:13:07.332 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.335 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
11:13:07.335 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #5
11:13:07.335 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.363 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #3
11:13:07.363 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.378 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #1
11:13:07.378 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.392 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #4
11:13:07.392 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.417 [main] INFO a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
11:13:07.417 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 0
11:13:07.418 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
11:13:07.418 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.439 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #2
11:13:07.439 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.453 [main] INFO a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
11:13:07.453 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 0
11:13:07.454 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 1: picking a transition out of 6 transition(s)
11:13:07.471 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #1
11:13:07.471 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.494 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #5
11:13:07.494 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.533 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #0
11:13:07.534 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.611 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #3
11:13:07.611 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.635 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #2
11:13:07.635 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.667 [main] INFO a.f.a.t.b.SeqModelChecker - State 2: Checking 1 state invariants
11:13:07.668 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 0
11:13:07.669 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #4
11:13:07.669 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.705 [main] INFO a.f.a.t.b.SeqModelChecker - State 2: Checking 1 state invariants
11:13:07.705 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 0
11:13:07.707 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 2: picking a transition out of 6 transition(s)
11:13:07.730 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #0
11:13:07.730 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.779 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #3
11:13:07.780 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.809 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #2
11:13:07.809 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.849 [main] INFO a.f.a.t.b.SeqModelChecker - State 3: Checking 1 state invariants
11:13:07.849 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 3: Checking state invariant 0
11:13:07.851 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #4
11:13:07.851 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.886 [main] INFO a.f.a.t.b.SeqModelChecker - State 3: Checking 1 state invariants
11:13:07.886 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 3: Checking state invariant 0
11:13:07.889 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #5
11:13:07.889 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.935 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #1
11:13:07.936 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:07.962 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 3: picking a transition out of 6 transition(s)
11:13:07.987 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #2
11:13:07.987 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.038 [main] INFO a.f.a.t.b.SeqModelChecker - State 4: Checking 1 state invariants
11:13:08.038 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 4: Checking state invariant 0
11:13:08.042 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #0
11:13:08.042 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.098 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #1
11:13:08.098 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.131 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #3
11:13:08.131 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.165 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #4
11:13:08.165 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.200 [main] INFO a.f.a.t.b.SeqModelChecker - State 4: Checking 1 state invariants
11:13:08.200 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 4: Checking state invariant 0
11:13:08.220 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #5
11:13:08.220 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.276 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 4: picking a transition out of 6 transition(s)
11:13:08.305 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #0
11:13:08.305 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.376 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #2
11:13:08.376 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.435 [main] INFO a.f.a.t.b.SeqModelChecker - State 5: Checking 1 state invariants
11:13:08.435 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 5: Checking state invariant 0
11:13:08.464 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #3
11:13:08.464 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.506 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #1
11:13:08.506 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.592 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #5
11:13:08.593 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.670 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #4
11:13:08.670 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:08.706 [main] INFO a.f.a.t.b.SeqModelChecker - State 5: Checking 1 state invariants
11:13:08.706 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 5: Checking state invariant 0
11:13:09.176 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 5: picking a transition out of 6 transition(s)
11:13:09.210 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #2
11:13:09.210 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:09.278 [main] INFO a.f.a.t.b.SeqModelChecker - State 6: Checking 1 state invariants
11:13:09.278 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 6: Checking state invariant 0
11:13:09.414 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #4
11:13:09.414 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:09.450 [main] INFO a.f.a.t.b.SeqModelChecker - State 6: Checking 1 state invariants
11:13:09.450 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 6: Checking state invariant 0
11:13:11.205 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #0
11:13:11.206 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:11.278 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #5
11:13:11.278 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:11.353 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #3
11:13:11.353 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:11.401 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #1
11:13:11.401 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:11.448 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 6: picking a transition out of 6 transition(s)
11:13:11.489 [main] INFO a.f.a.t.b.SeqModelChecker - ----------------------------
11:13:11.489 [main] INFO a.f.a.t.b.SeqModelChecker - Symbolic runs left: 98
11:13:11.489 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
11:13:11.489 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
11:13:11.494 [main] ERROR a.f.a.t.Tool\$ - <unknown>: internal error: SMT 0: Declaring cell 5, while cell 21799 has been already declared. Damaged arena?
at.forsyte.apalache.infra.AdaptedException: <unknown>: internal error: SMT 0: Declaring cell 5, while cell 21799 has been already declared. Damaged arena?
at at.forsyte.apalache.infra.Executor.run(Executor.scala:37)
at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:83)
at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:135)
at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:115)
at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:36)
at at.forsyte.apalache.tla.Tool.main(Tool.scala)
System information
- Apalache version:
v0.27.0-2-g09ff5045d build v0.27.0-2-g09ff5045d - OS:
Mac OS X - JDK version:
17.0.2
Odd that this happens on simulate but not on check. At least here (on my local setup) the error happens consistently on the third symbolic run.
