Missformed SMT source in ((_ map or) (store ((as const (Array Int Bool)) false) 0 true)

[vkuncak]

With Z3 version 4.14.1 - 64 bit on macOS with M4 Pro, one test case fails:

[info] -  15: SAT - Sorted.scala-0.tip solver=no-inc:smt-z3 *** FAILED *** (98 milliseconds)
[info]   inox.solvers.smtlib.MissformedSMTException: Missformed SMT source in ((_ map or) (store ((as const (Array Int Bool)) false) 0 true) (store ((as const (Array Int Bool)) false) 26285 true)):
[info] Unknown SMT term of class: class smtlib.trees.Terms$FunctionApplication:
[info] ((_ map or) (store ((as const (Array Int Bool)) false) 0 true) (store ((as const (Array Int Bool)) false) 26285 true))
[info]   at inox.solvers.smtlib.SMTLIBParser.fromSMT(SMTLIBParser.scala:276

[sankalpgambhir]

This was reproduced on our CI on Linux, JDK 17, with z3 4.15.1, so the issue is not immediately platform, JDK, or z3 version sensitive. It is, however, inconsistent.

https://github.com/epfl-lara/inox/actions/runs/17563377508/job/49884856919#step:11:4798