Nikolaj Bjorner

I tried the latest change. It still diverges depending on which random seed is used. So the change doesn't address the main cause and I posted a head's up that...

Thanks @levnach! For @zvonimir: if you get a chance to try other regression tests with the default arithmetic solver setting it would be great to know about other places that...

Ok, thanks. We will carve out some time to go through this. If you have a chance to assemble a few more samples it could help to prepare for this...

I pushed a change that improves the picture somewhat on the attached example. It possibly doesn't address the root cause, but debugging the file revealed a way the solver could...

Nice benchmarking infrastructure! The scatter plot looks a little too uniform to be believable. So there is a chance that some parameters got ignored or overwritten or omitted. I typically...

If you have a way to retrieve SMT2 files it also helps. For the particular case of the last example, it matters a lot which random seed I use. It...

I use statistics and look for characteristics. New solver (look for propagations-cheap) ``` (:added-eqs 2632 :arith-eq-adapter 163 :arith-assume-eqs 1 :arith-bound-propagations-cheap 1149 :arith-bound-propagations-lp 995 :arith-cheap-eqs 11 :arith-conflicts 1980 :arith-diseq 238 :arith-grobner-calls...

Sometimes taking shorter running examples that show average regressions is easier. For example these ones: aws_byte_buf_append_dynamic_harness.ymltrue true 18.0  19.1  99.8 true 11.0  12.7  95.2 aws_priority_queue_remove_harness.ymltrue true 26.9  27.9  178   true...

Yes please, exactly these ones or 3-6 of them, such as: aws_priority_queue_push_ref_harness.yml aws_byte_buf_reset_harness.yml aws_priority_queue_push_harness.yml as SMTLIB2 commands, ....

For your piro.txt case: it is indeed fairness. Generally the new solver is much faster, but then gets trapped in some cases during non-linear lemma generation. It seems to indicate...