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