Z3Prover
Z3 4.8.14 concludes input file is `unsat`, but loops forever on 4.15.1
When attempting to upgrade from Z3 4.8.14 to 4.15.1, we noticed that an SMT interaction that used to terminate (culminating in Z3 printing unsat) in about 3 seconds with Z3 4.8.14 now goes into an infinite loop when attempting the same thing with Z3 4.15.1. I have attached the input .smt file here (test.smt2.tar.gz), which is 964 lines long. (I was unsuccessful in minimizing the input program with ddSMT, which failed to produce any results after running it for a week, but perhaps there are other things that could be tried to minimize this.)
This particular formula benefits from rewriting simplification with the flag: rewriter.bv_sort_ac=true
z3 test.smt2 /v:10 rewriter.bv_sort_ac=true (simplifier :num-exprs 1 :num-asts 54524 :time 0.09 :before-memory 21.23 :after-memory 23.99) unsat
Otherwise, it expands.
@NikolajBjorner these files are automatically generated by a tool. If this is not a bug, is there a guideline as to when we should pass this flag? Is there a reason to not always do this?
We are seeing a similar issue - proofs that previously ran OK with z3 4.13.x are now blowing up in execution time and memory consumption with z3 4.15.0.
Are there any known memory leak issues in 4.15.x? (I've tried 4.15.2 and it made no difference...)
