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

merge

Browse source 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-11 14:14:44 -08:00
commit 1e22cb73d5
4 changed files with 16 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_asymm_branch.cpp
View file

@ -208,7 +208,6 @@ namespace sat {
m_to_delete.reset();
for (unsigned i = m_pos.size() - 1; i-- > 0; ) {
literal lit = m_pos[i];
//SASSERT(scc.get_left(lit) < scc.get_left(last));
int right2 = scc.get_right(lit);
if (right2 > right) {
// lit => last, so lit can be deleted
@ -345,10 +344,12 @@ namespace sat {
bool asymm_branch::process_sampled(scc& scc, clause & c) {
scoped_detach scoped_d(s, c);
sort(scc, c);
#if 0
if (uhte(scc, c)) {
scoped_d.del_clause();
return false;
}
#endif
return uhle(scoped_d, scc, c);
}