Performance of FunctionSymbol.checkSort

[stahlbauer]

In our application, we construct huge formulas where already the construction process takes thousands of seconds. The function FunctionSymbol.checkSort is a huge bottleneck in this case. Is the .toString() for comparing types really necessary? The formula consists of boolean variables only; why is it necessary to have the type check in this case?

[stahlbauer]

Loading a formula in CNF (dimacs with approx 300k lines) with Z3 (and converting it to the corresponding solver-representation) takes less than two seconds, whereas SMTInterpol needs several minutes for the same job.

[jhoenicke]

The toString() method should only be called if is a type error. I noticed it may also be called for LIRA logic if implicit int to real casts appear. This should be fixed, but I doubt that is your problem since you are only using boolean variables. Do you have an example that triggers this problem?