mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 01:11:55 +00:00
Code Activity

use a faster version of get_model in debug checks

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-10 11:57:33 -07:00 • committed by Lev Nachmanson
parent 2e957a97cf
commit e1d3119f9f
2 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/util/lp/lar_solver.h
View file

@ -1190,6 +1190,7 @@ public:
void get_model(std::unordered_map<var_index, mpq> & variable_values) const;
void get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const;
void get_model(std::unordered_map<var_index, mpq> & variable_values) const {
mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes