Unhandled Z3Exception with arrays encoding: domain <> parameter sort mismatch

[thpani]

Description

One more from #1588:
Checking with arrays throws an unhandled Z3Exception on the spec below.

Input specification

https://gist.github.com/thpani/a629c9a01530160f7981a6f51becebb1

The command line parameters used to run the tool

--smt-encoding=arrays

Expected behavior

No unhandled exception :)
Probably this should fail on picking from the function set.

Log files

12:17:43.074 [main] INFO  a.f.a.t.Tool$ - Checker options: check --smt-encoding=arrays Oracle.tla
12:17:43.077 [main] INFO  a.f.a.t.Tool$ - Tuning: 
12:17:43.080 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
12:17:43.408 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
12:17:43.411 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
12:17:43.411 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
12:17:43.752 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Your types are purrfect!
12:17:43.753 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > All expressions are typed
12:17:43.755 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
12:17:43.755 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass
12:17:43.762 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Oracle.cfg: Loading TLC configuration
12:17:43.767 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > No TLC configuration found. Skipping.
12:17:43.768 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --init is not set. Using Init
12:17:43.768 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --next is not set. Using Next
12:17:43.768 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
12:17:43.768 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
12:17:43.777 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK]
12:17:43.777 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass
12:17:43.778 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
12:17:43.786 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK]
12:17:43.786 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass
12:17:43.787 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next
12:17:43.809 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass [OK]
12:17:43.809 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass
12:17:43.812 [main] INFO  a.f.a.t.a.p.PrimingPassImpl -   > Introducing InitPrimed for Init'
12:17:43.816 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass [OK]
12:17:43.816 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #6: VCGen
12:17:43.817 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > No invariant given. Only deadlocks will be checked
12:17:43.817 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: VCGen [OK]
12:17:43.817 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass
12:17:43.817 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
12:17:43.822 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
12:17:43.822 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
12:17:43.824 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
12:17:43.825 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
12:17:43.829 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
12:17:43.832 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
12:17:43.838 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
12:17:43.845 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass [OK]
12:17:43.845 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass
12:17:43.862 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 1 initializing transitions
12:17:43.868 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 1 transitions
12:17:43.868 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > No constant initializer
12:17:43.872 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Applying unique renaming
12:17:43.879 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass [OK]
12:17:43.879 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass
12:17:43.883 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
12:17:43.884 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
12:17:43.885 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
12:17:43.886 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
12:17:43.886 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
12:17:43.887 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass [OK]
12:17:43.887 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass
12:17:43.889 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
12:17:43.891 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
12:17:43.891 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
12:17:43.892 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
12:17:43.894 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
12:17:43.898 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
12:17:43.898 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass [OK]
12:17:43.899 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat
12:17:43.899 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Running Snowcat .::.
12:17:44.142 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Your types are purrfect!
12:17:44.142 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > All expressions are typed
12:17:44.143 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat [OK]
12:17:44.144 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #12: BoundedChecker
12:17:45.759 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
12:17:45.760 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
12:17:45.822 [main] ERROR a.f.a.t.Tool$ - Unhandled exception
com.microsoft.z3.Z3Exception: domain sort Cell_F%Sb_%Si and parameter sort (Array (Array Bool Int) Bool) do not match
	at com.microsoft.z3.Native.mkStore(Native.java:4107)
	at com.microsoft.z3.Context.mkStore(Context.java:1775)
	at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.mkStore(Z3SolverContext.scala:247)
	at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.toExpr(Z3SolverContext.scala:714)
	at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.assertGroundExpr(Z3SolverContext.scala:306)
	at at.forsyte.apalache.tla.bmcmt.smt.RecordingSolverContext.assertGroundExpr(RecordingSolverContext.scala:157)
	at at.forsyte.apalache.tla.bmcmt.rules.SetCtorRule.$anonfun$apply$4(SetCtorRule.scala:43)
	at at.forsyte.apalache.tla.bmcmt.rules.SetCtorRule.$anonfun$apply$4$adapted(SetCtorRule.scala:41)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at at.forsyte.apalache.tla.bmcmt.rules.SetCtorRule.apply(SetCtorRule.scala:41)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:349)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:382)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:416)
	at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.apply(QuantRule.scala:47)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:349)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:382)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:416)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.mapArg$1(AndRule.scala:63)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.$anonfun$apply$2(AndRule.scala:67)
	at scala.collection.immutable.List.map(List.scala:246)
	at scala.collection.immutable.List.map(List.scala:79)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.apply(AndRule.scala:67)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:349)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:382)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:416)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.prepareTransition(TransitionExecutorImpl.scala:106)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.prepareTransition(FilteredTransitionExecutor.scala:41)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.prepareTransition(ConstrainedTransitionExecutor.scala:97)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6(SeqModelChecker.scala:179)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6$adapted(SeqModelChecker.scala:173)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:926)
	at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:896)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:173)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:95)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:56)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:129)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:84)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:22)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.$anonfun$run$3(PassChainExecutor.scala:45)
	at scala.Option.flatMap(Option.scala:283)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.$anonfun$run$1(PassChainExecutor.scala:44)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:169)
	at scala.collection.LinearSeqOps.foldLeft$(LinearSeq.scala:165)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:38)
	at at.forsyte.apalache.tla.Tool$.runAndExit(Tool.scala:177)
	at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:256)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$2(Tool.scala:119)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$2$adapted(Tool.scala:119)
	at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:414)
	at at.forsyte.apalache.tla.Tool$.runForModule(Tool.scala:404)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:119)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:52)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
12:17:45.824 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  3 sec
12:17:45.825 [main] INFO  a.f.a.t.Tool$ - Total time: 3.351 sec

System information

• Apalache version: v0.24.1-98-g263c2a60a build v0.24.1-98-g263c2a60a:
• OS: Mac OS X:
• JDK version: 17.0.2: