mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-22 11:07:51 +00:00
Code Activity

fix drat generation in asymmetric branch simplification

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-12 13:19:09 -08:00
parent f835a3c2b2
commit dc5e4ca1c5
3 changed files with 32 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/sat/sat_drat.cpp
View file

@ -585,8 +585,21 @@ namespace sat {
void drat::del(clause& c) {
#if 0
// check_duplicates:
for (literal lit : c) {
VERIFY(!m_seen[lit.index()]);
m_seen[lit.index()] = true;
}
for (literal lit : c) {
m_seen[lit.index()] = false;
}
#endif
TRACE("sat", tout << "del: " << c << "\n";);
if (m_out) dump(c.size(), c.begin(), status::deleted);
if (m_out) {
dump(c.size(), c.begin(), status::deleted);
}
if (m_check) {
clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned());
append(*c1, status::deleted);