Soundness bug in QF_NIA

[wintered]

z3 smt.arith.solver=2 returns the correct result while z3 without options is at fault.

[761] % z3 small.smt2
sat
[762] % z3 smt.arith.solver=2 small.smt2
unsat
[763] % cvc4 -q small.smt2
unsat
[764] % 
[764] % cat small.smt2
(declare-fun a () Int)
(assert (distinct 0 (div 0 a)))
(assert (= 0 (div (- (* a a) a) a)))
(check-sat)
[765] %

OS: Ubuntu 18.04 Commit: 3cae0b4

[NikolajBjorner]

@levnach Tracing has a side-effect on the solver.

C:\zzz\build>z3 3896.smt2 smt.arith.solver=6 /tr:arith unsat

C:\zzz\build>z3 3896.smt2 smt.arith.solver=6 sat

I narrowed it to running this code

        if (m_solver) {
            out << lp().constraints();
            lp().print_terms(out);
            // the tableau
            auto pp = lp ::core_solver_pretty_printer<lp::mpq, lp::impq>(
                lp().m_mpq_lar_core_solver.m_r_solver, out);
            pp.print();
            for (unsigned j = 0; j < lp().number_of_vars(); j++) {
                lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
            }
        }

[NikolajBjorner]

@levnach could you review the solver for side-effects in the print routines? Otherwise the soundness seems fixed by cd98a2198

[levnach]

@NikolajBjorner , Do you still suspect the side effects of printing in lar_solver?