Odd behavior difference Windows and MacOS

[mrkmarron]

Running the attached file on Windows and MacOS has very different behavior. On Windows it immediately returns SAT (as expected) while on MacOS (M1 ARM64) it runs until a timeout hits. Additionally, if line 700 is changed to replace the constant @BLENMAX with the literal value 32 the solver can immediately find the SAT solution. Further this function is never referenced anywhere else in the file (so could be deleted entirely and is clearly semantically irrelevant).

Given these behaviors I am suspicious there is more going on here (like an ARM64 bug) than just bad luck with heuristics or solver ordering.

Build configuration for M1 is:
CXX=clang++ CC=clang FPMATH_ENABLED=False python scripts/mk_make.py --arm64=true --staticlib

build.smt2.txt

[mrkmarron]

This example might also be relevant as it fails with a timeout (or "smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)") when the lambdas on lines 958 and 1643 are replaced by the empty list values. These clauses are not meaningful to the result as they are always successful given the structure of the formula.

(Behavior appears on both Windows and MacOS).

unknown.smt2.txt

[NikolajBjorner]

For the first one, some bisection debugging would be useful.

• build debug version on M1, or at least with trace enabled
• build debug version on your x64 platform
• run both version with -tr:mk_var_bug or -tr:context or -tr:seq to identify first place where traces differ
• narrow with breakpoints and other traces

Perhaps it is easier than that and pre-processing is where the platform dependency comes in.
The first few lines of verbose -v:10 gives an idea if this is the case.

C:\z3\build>..\release\z3 build.smt2 /v:1 smt.random_seed=6 /v:10
(simplifier :num-exprs 821 :num-asts 5249 :time 0.00 :before-memory 19.70 :after-memory 19.70)
(simplifier :num-exprs 821 :num-asts 5248 :time 0.00 :before-memory 19.70 :after-memory 19.70)
(propagate-values :num-exprs 661 :num-asts 5183 :time 0.00 :before-memory 19.70 :after-memory 19.82)
(ctx-simplify :num-steps 6776)
(ctx-simplify :num-exprs 780 :num-asts 5914 :time 0.00 :before-memory 19.82 :after-memory 19.91)
(simplifier :num-exprs 780 :num-asts 5578 :time 0.00 :before-memory 19.82 :after-memory 19.82)
(solve_eqs :num-exprs 724 :num-asts 5708 :time 0.00 :before-memory 19.82 :after-memory 19.82)
(:num-elim-vars 23)
(elim-uncnstr :num-exprs 724 :num-asts 5708 :time 0.00 :before-memory 19.82 :after-memory 19.82)

Note that build.smt2.txt behaves differently depending on the random seed.
However, we do want the solver to produce the same results regardless of platforms (so not use certain std features that are platform dependent).

[mrkmarron]

After some investigation I am noticing 2 interesting things.

1. The solver gets stuck in the search looping trying to complete the arith model but failing in the final_check loop. Seems to be some issues with how map and contains interact and it (seems?) like it keeps trying to extend the model even though the sequence size is fixed as a constant 3 elements.

2. If I replace the use of the lambdas or the seq.contains in the attached smt2 file (957/963 and 1646/1652) with the manually unrolled versions then the proof will terminate with unknown and a report of unhandled quantifiers. The unknown quantifiers do not exist explicitly in the SMT file but are introduced as forall expressions in the internalize_assertions that the solver generates and have a qid of :lambda-def.

I am wondering if these quantifiers are also causing the instability in (1) and am not sure why/how they are getting created as I thought map/lambda were processed as rewrites.

unknown2.smt2.txt

[NikolajBjorner]

the "unknown" result turns out to be subtle: there is an internal model check call that is invoked. It determines somehow that the model built doesn't satisfy the assignment to a ground literal so it bails out. Needs investigation.

[NikolajBjorner]

There were several bugs related to incomplete handling of map/fold operations and even creation of ill-formed terms.
A sequence of commits tries to address the issues:

809838f
53611f4
7a55bd5
3900c03
6df7112
8311525
0629353

I also added initial unit tests for map/mapi/fold/foldi.
It would be great to add more tests at this level (and not relying purely on end-to-end testing).

Z3Prover/z3test@d32176e

[mrkmarron]

Just built this and ran tests. It looks like all the issues I had found have been cleared up. I'll plan to workup some tests for these features too.