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

disable a check

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-13 15:36:01 -10:00 • committed by Lev Nachmanson
parent 267457aaf4
commit ad98594447
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/util/lp/nla_solver.cpp
View file

@ -849,7 +849,6 @@ struct solver::imp {
// x is equivalent to y if x = +- y // x is equivalent to y if x = +- y
void init_vars_equivalence() { void init_vars_equivalence() {
SASSERT(abs_values_table_is_ok());
TRACE("nla_solver",); TRACE("nla_solver",);
SASSERT(m_vars_equivalence.empty()); SASSERT(m_vars_equivalence.empty());
collect_equivs(); collect_equivs();
@ -858,7 +857,7 @@ struct solver::imp {
m_vars_equivalence.register_var(j, vvr(j)); m_vars_equivalence.register_var(j, vvr(j));
} }
SASSERT(tables_are_ok()); SASSERT((m_lar_solver.settings().random_next() % 100) || tables_are_ok());
} }
bool vars_table_is_ok() const { bool vars_table_is_ok() const {