mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
c71da17a10
commit
5af139055d
|
@ -41,7 +41,7 @@ namespace sat {
|
|||
unsigned nc = s.m_stats.m_num_cuts - m_num_cuts;
|
||||
unsigned ni = s.m_stats.m_num_learned_implies - m_num_learned_implies;
|
||||
IF_VERBOSE(2,
|
||||
verbose_stream() << "(sat.aig-simplifier";
|
||||
verbose_stream() << "(sat.cut-simplifier";
|
||||
if (nu > 0) verbose_stream() << " :num-units " << nu;
|
||||
if (ne > 0) verbose_stream() << " :num-eqs " << ne;
|
||||
if (ni > 0) verbose_stream() << " :num-bin " << ni;
|
||||
|
@ -475,7 +475,7 @@ namespace sat {
|
|||
}
|
||||
++i;
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.aig-simplifier num simulated eqs " << num_eqs << ")\n");
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.cut-simplifier num simulated eqs " << num_eqs << ")\n");
|
||||
}
|
||||
|
||||
void cut_simplifier::track_binary(bin_rel const& p) {
|
||||
|
|
|
@ -252,7 +252,7 @@ private:
|
|||
SASSERT(is_uninterp_const(e));
|
||||
func_decl* f = to_app(e)->get_decl();
|
||||
|
||||
if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) {
|
||||
if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2 && m_arith.is_int(e)) {
|
||||
func_decl* fbv;
|
||||
rational offset;
|
||||
if (!m_int2bv.find(f, fbv)) {
|
||||
|
|
Loading…
Reference in a new issue