Wrong output of ctx-solver-simplify called via Java-API?

[micha-78]

Hi there,

we've been running into rather strange results when using Z3 to simplify some formulas. We've broken it down to a very simple example - to simplify the expression a==0 || b==0 || b==0 Clearly, this is the same as omitting the last (duplicate) term, i.e., a==0 || b==0

When we try to simplify this with https://rise4fun.com/z3, everything is fine: https://rise4fun.com/Z3/MDlO

(goals
(goal
  (or (= a #x00000001) (= b #x00000000))
  :precision precise :depth 1)
)

However, when using the Java API, ctx-solver-simplify generates an invalid result, while simplify or ctx-simplify give the expected result.

Here is our code:

    Context context = new Context();

    // a=1
    Expr var1 = context.mkBVConst("a", 32);
    Expr val1 = context.mkBV("1", 32);
    BoolExpr eq1 = context.mkEq(var1, val1);

    // b=0
    Expr var2 = context.mkBVConst("b", 32);
    Expr val2 = context.mkBV("0", 32);
    BoolExpr eq2 = context.mkEq(var2, val2);

    // a=1 || b=0  
    BoolExpr or1 = context.mkOr(eq1, eq2);

    // b=0
    Expr val3 = context.mkBV("0", 32);
    BoolExpr eq3 = context.mkEq(var2, val3);

    // (a=1 || b=0) || b=0
    BoolExpr z3Expr = context.mkOr(or1, eq3);
    Goal goal = context.mkGoal(true, false, false);
    goal.add(z3Expr);

    Tactic simplify = context.mkTactic("simplify");
    Tactic ctxSimplify = context.mkTactic("ctx-simplify");
    Tactic ctxSolverSimplify = context.mkTactic("ctx-solver-simplify");

    ApplyResult res1 = simplify.apply(goal);
    ApplyResult res2 = ctxSimplify.apply(goal);
    ApplyResult res3 = ctxSolverSimplify.apply(goal);

    System.out.println("original term:\n" + z3Expr + "\n");
    System.out.println("simplify:\n" + res1 + "\n");
    System.out.println("ctxSimplify:\n" + res2 + "\n");
    System.out.println("ctxSolverSimplify:\n" + res3 + "\n");

    context.close();

The output:

original term:
(or (= a #x00000001) (= b #x00000000) (= b #x00000000))

simplify:
(goals
(goal
  (or (= a #x00000001) (= b #x00000000)))
)

ctxSimplify:
(goals
(goal
  (or (= a #x00000001) (= b #x00000000)))
)

ctxSolverSimplify:
(goals
(goal
  (= a #x00000001))
)

We tried 4.8.5 and 4.8.7, both versions show this behaviour.

Is this a problem with ctx-solver-simplify, or is there some problem with our code?

Thank you very much in advance!

[micha-78]

Thank you very much for the quick fix @NikolajBjorner - problem is solved in nightly. Do you already have a schedule for a post-4.8.7-release containing the fix? We prefer using a stable release of z3 instead of a nightly build in production.

[NikolajBjorner]

Would be good to address some of the arithmetic issues that are pending (and strings if possible). Albeit, no release is going to be perfect so based on your request I could set it off on next Monday (during a flight).

[micha-78]

For us, it would be great to have a release soon - however, if the code is not ready for a release yet, we will wait until it is, so do not rush it if you raise concerns about a quick release.

[micha-78]

@NikolajBjorner Could you please give us an update on how the status currently is? Are there still many bugs you plan to resolve before pushing a release?