z3 hangs forever

[ramanuj1729]

Consider the smt2 file generated with the help of Klee.

I am trying to evaluate it using z3 [version 4.8.5 - 64 bit]. However, z3 hangs forever. Specifically, when the formula is UNSAT z3 runs forever and does not produce any result.

Is formula size is big?
Is there any issue while using logic theory AUFBV?
May I get some suggestions to improve the z3 performance.

Each assert statement having some common subexpression. Is it possible to improve the z3 performance by solving subexpression separately?

Note: There is no issue with Klee. I am not able to get an idea that if I give this file to z3 as input then it fails and hags forever. Note that formula is UNSAT but z3 hangs. If I modify some condition to make it SAT then z3 also reports SAT and produce a model also.

SMT 2 FILE: z3Input_2.txt

[ramanuj1729]

Many thanks for looking at the issue. However, when I use updated Z3 [version 4.8.6 - 64 bit] to evaluate the different SMT2 file then z3 still hangs forever. I have attached the new SMT2 file. I have noticed that when a formula is UNSAT then only z3 hangs. I suspect that there is some issue while using logic theory AUFBV in z3.

SMTLIB2 File: z3InputNew.txt

[NikolajBjorner]

It just happens to be tough to solve. I see a bunch of multipliers.
The examples illustrated that Z3 could detect benchmarks that are in reality pure bit-vector formulas.
More generally, if you have array store and select over many different arguments the current transformation does not take effect and you will be using the slower more general purpose solver.
Note also that you can throw all your cores at this problem by setting parallel.enable=true.