regression with arith.solver=6

[mtzguido]

Hi, we found this failure while upgrading F* projects, specifically HACL* to Z3 4.13.3. Some files were taking considerably longer times when compared to Z3 4.8.5 (>1 hour from just a minute or two), and failing instead of succeeding.

Here's one somewhat distilled example (still running ddsmt to minimize further). hacl-min.smt2.txt

I bisected the issue but I don't think it's very useful. It points to 28c827f:

# first bad commit: [28c827fb69b3de2449044dedf62233c09e658ee1] fix #2919

Specifically it seems to be this chunk of it
28c827f#diff-1e1c1b4bddfd09f68a39e64cf5fcda0bb3bec7306f9c8548fa2a081e5afab4f8L840-R840

-            if (st.m_num_non_linear != 0 && st.m_has_int) 
-                m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
-            else 
-                setup_lra_arith();
+            setup_lra_arith();

which I think is just making sure that solver=6 is respected.

(Also, even if Z3 fails here, it seems to take a really long time for the rlimit we give it, so I suspect there's also an rlimit leak here somewhere. Or the units are very different between solver 2 and 6.)

Some more context: hacl-star/hacl-star#1014

[levnach]

Here some first observations. In the current master the long run does not happen but instead I get an "unknown". It seems it is extremely rare occurrence as well.
Running the master release for random seeds 0-10000 the timeout of 20 seconds produced 10001 unsats very fast. I will try to figure out the origin of "unknown"

[mtzguido]

Smaller version: full_min.smt2.txt (ddsmt still churning)
Ah, nevermind, ddsmt reduced the rlimit and this does not really show the same problem.

[mtzguido]

I'm not sure how helpful this is, but here's a smaller file that runs much slower with solver 6 than 2... but only with few seeds (e.g. 0), and it does say unsat eventually.
hacl-min-try4.smt2.txt

[NikolajBjorner]

C:\z3\release>z3 C:\users\nbjorner\Downloads\hacl-min-try4.smt2.txt /st smt.arith.nl.nra=false
unsat this works quite well. So we spend too much time in nra_solver for this one.

[mtzguido]

Here is another very noticeable difference between the solvers: hacl-glv-divergence.smt2.txt. Solver 2 (and Z3 4.8.5) come back quickly with unsat. Current Z3 takes several minutes (at least 30). Reducing the rlimit by 10x still works in 4.8.5 and solver 2, but fails in master in ~4minutes.

I bisected the difference to this patch: 5177cc4, which changes the ordering of subterms in disjunctions (I think?). We've previously added an option to disable that sorting (PR #6774), and I am disabling it in this file, but it doesn't seem to help here.

I can't say I understand why a huge discrepancy is caused by this ordering... I could try to investigate more with some guidance.

[NikolajBjorner]

Past experience with this was that it has to do with patterns and relevancy: if the right literals become relevant, E-matching may trigger and complete the proof. If literals are compiled in a different order, this doesn't happen.
Given that F* uses case-split = 3 and other operational features I would first assume it has to be something you can solve by encoding formulas. Beyond that one way to debug further is to take the bisection point and run --trace on both versions. The axiom profiler or debug trace output should indicate points of divergence. Not necessarily user-friendly investigation.
Also, good if we can learn something about making instantiation more stable. @CanCebeci may find this use case useful too.

[mtzguido]

Here's a fresh example from @cmovcc, heavily minimized.

(set-option :global-decls false)
(set-option :smt.mbqi false)
(set-option :auto_config false)
(set-option :produce-unsat-cores true)
(set-option :model true)
(set-option :smt.case_split 3)
(set-option :smt.relevancy 2)
(set-option :rewriter.enable_der false)
(set-option :rewriter.sort_disjunctions false)
(set-option :pi.decompose_patterns false)

(declare-sort Term)

(declare-fun Box (Int) Term)

(declare-fun Box_proj_0 (Term) Int)
(assert
 (! (forall ((@u0 Int))
   (! (= (Box_proj_0 (Box @u0)) @u0)
    :pattern ((Box @u0))
    :qid projection_inverse_Box_proj_0))
  :named projection_inverse_Box_proj_0))

(declare-fun Prims.op_add (Term Term) Term)
(declare-fun Prims.op_mod (Term Term) Term)
(declare-fun Prims.op_mul (Term Term) Term)

(assert
 (!
  (forall ((@x0 Term) (@x1 Term))
   (! (= (Prims.op_add @x0 @x1) (Box (+ (Box_proj_0 @x0) (Box_proj_0 @x1))))
    :pattern ((Prims.op_add @x0 @x1))
    :qid primitive_Prims.op_add))
  :named primitive_Prims.op_add))

(assert
 (!
  (forall ((@x0 Term) (@x1 Term))
   (! (implies
     (not (= (Box_proj_0 @x1) 0))
     (= (Prims.op_mod @x0 @x1) (Box (mod (Box_proj_0 @x0) (Box_proj_0 @x1)))))
    :pattern ((Prims.op_mod @x0 @x1))
    :qid primitive_Prims.op_mod))
  :named primitive_Prims.op_mod))

(assert
 (!
  (forall ((@x0 Term) (@x1 Term))
   (! (= (Prims.op_mul @x0 @x1) (Box (* (Box_proj_0 @x0) (Box_proj_0 @x1))))
    :pattern ((Prims.op_mul @x0 @x1))
    :qid primitive_Prims.op_mul))
  :named primitive_Prims.op_mul))

(declare-const @x0 Term)
(declare-const @x1 Term)

(assert (= (Prims.op_add (Prims.op_mul @x0 @x0) (Box 1)) (Prims.op_mul (Box 4) @x1)))
(assert (not (= (Prims.op_mod (Prims.op_mul @x0 @x0) (Box 4)) (Box 3))))

(set-option :rlimit 2500000)
(check-sat)

It states the nonlinear fact x*x+1 = 4y ==> x*x % 4 = 3

It is very fast and robust with solver=2:

$ time for seed in $(seq 0 499) ; do z3-master smt.arith.solver=2 smt.random_seed=$seed antonin.smt2 | tail -n1; done | sort | uniq -c
    500 unsat

real    0m2.662s
user    0m1.225s
sys     0m1.830s

But performs badly with 6:

$ time for seed in $(seq 0 499) ; do z3-master smt.arith.solver=6 smt.random_seed=$seed antonin.smt2 | tail -n1; done | sort | uniq -c
    280 unknown
    220 unsat

real    0m53.307s
user    0m51.720s
sys     0m2.926s

This is on Z3 master.

[mtzguido]

Wow, actually, it seems to change wildly according to whether unsat cores are being produced or not. Removing all of the options at the top of the file makes it work reliably with 6 again:

$ time for seed in $(seq 0 999) ; do z3-master smt.arith.solver=6 smt.random_seed=$seed antonin.smt2 | tail -n1; done | sort | uniq -c
   1000 unsat

real    0m5.741s
user    0m2.812s
sys     0m3.708s

But enabling unsat cores gives:

$ time for seed in $(seq 0 999) ; do z3-master smt.arith.solver=6 smt.random_seed=$seed antonin.smt2 | tail -n1; done | sort | uniq -c
    553 unknown
    447 unsat

real    1m45.672s
user    1m42.560s
sys     0m5.779s

Related to #7538

[NikolajBjorner]

nlsat considered harmful:
there is a combination of "theories": quantifiers and non-linear arithmetic.
At some point the nla_core is asked to solve something it cannot solve, but quantifier instantiation or other theories are on stand-by to instantiate useful lemmas. If we enable nlsat to really provide a decisive answer it spins off in a place it cannot figure out this lemma. If we disable nlsat (smt.arith.nl.nra=false) it just returns unknown and lets the quantifier instantation do its magic.

Takeaways?

• maybe tell the nla core that it doesn't have to work too hard in this round because there are other activities that can make progress.
• maybe figure out what lemmas are missing. Nominally, we should have some lemmas for squares and congruences. https://z3prover.github.io/slides/guest-lectures-wien-2025/lecture4-arithmetic.html#/sec-euclidian-lemmas-ii, but are they misconfigured or just inadequate?