mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

improve comments for scoped_weakness

Browse source
This commit is contained in:
Arie Gurfinkel 2017-09-06 17:39:13 -04:00
parent 890bc0f7c9
commit 321cad70d6
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/spacer_prop_solver.h
View file

@ -144,9 +144,11 @@ public:
public: public:
scoped_weakness(prop_solver &ps, unsigned solver_id, unsigned weakness) : scoped_weakness(prop_solver &ps, unsigned solver_id, unsigned weakness) :
m_params(*ps.m_fparams[solver_id == 0 ? 0 : 0 /*1*/]) { m_params(*ps.m_fparams[solver_id == 0 ? 0 : 0 /*1*/]) {
// save current values
m_arith_ignore_int = m_params.m_arith_ignore_int; m_arith_ignore_int = m_params.m_arith_ignore_int;
m_array_weak = m_params.m_array_weak; m_array_weak = m_params.m_array_weak;
// set values based on weakness score
m_params.m_arith_ignore_int = weakness < 1; m_params.m_arith_ignore_int = weakness < 1;
m_params.m_array_weak = weakness < 2; m_params.m_array_weak = weakness < 2;
} }