Bug with Z3 sorts / putting together a formula

[zhao-nan]

In my project, i want to translate expressions to Z3 and use the solver to check their validity / satisfiability.

I have a Z3AST init (and (= i 0) (= b false)) and a Z3AST pre (<= i 42). Now, as a test, I want to prove that init implies pre, so I call my Z3Context like this: z3Context.mkImplies(init, fpre)

However, this throws an unexpected exception:

Sort mismatch at argument #1 for function (declare-fun => (Bool Bool) Bool) supplied sort is Bool

Indeed, when debugging, I can see that getSort of both Z3ASTs is Bool, but for init, the value isBoolSort is false. I suspect this could point to the cause of the bug, but I'm stuck here. Can this be solved somehow?

[mario-bucev]

Hello! Could it be that something in init has a mismatched sort (e.g. i and 0 not being of the same sort)? For instance, this snippet works fine for me:

val z3 = new Z3Context("MODEL" -> true)
val intSort = z3.mkIntSort()
val boolSort = z3.mkBoolSort()
val i = z3.mkFreshConst("i", intSort)
val b = z3.mkFreshConst("b", boolSort)
val init = z3.mkAnd(z3.mkEq(i, z3.mkInt(0, intSort)), z3.mkEq(b, z3.mkFalse()))
val pre = z3.mkLE(i, z3.mkInt(42, intSort))

val solver = z3.mkSolver()
solver.assertCnstr(z3.mkNot(z3.mkImplies(init, pre)))
val (result, _) = solver.checkAndGetModel()
assert(result == Some(false))

[zhao-nan]

Hi, thank you very much for responding! I can reproduce your example too (with some adaptations; e.g. in my version of scalaz3, the solver does not have checkAndGetModel(), so I just use check). However, in my project, all the sorts seem to be correct as well, and z3 never complains when assembling the subformulas with mkEq, mkLE etc.. should there not be an exception or notification earlier if the types in the subformula do not match?

I also attach this debug screenshot where you can see that Bool is reported as the Sort of both formulas, but isBoolSort returns true only for the first one; for init, it is false.

Confusingly, replacing ìnit by something very simple, like z3.mkTrue(), does not help. Although fpre is reported to be true and fpre.getSort.isBoolSort is also true, the error described above still happens.

[mario-bucev]

Oops, checkAndGetModel is indeed private, I've tested it within the project and haven't thought about the accessibility, sorry for the confusion! It seems that fpre.context and init.context are not the same. Could it be that these are constructed with different Z3Context? In general, we use only one context (or one context per local usage).

[zhao-nan]

Ah, that's it! I was translating init and fpre somewhere else, and used a new context there. Thank you very much.