mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

local sat solver change

Browse source 
Signed-off-by: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
This commit is contained in:
unknown 2015-08-23 10:58:12 -07:00
parent a78fc031bc
commit 2b48092541
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_solver.cpp
View file

@ -2626,7 +2626,7 @@ namespace sat {
out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n"; out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
for (unsigned i = 0; i < m_trail.size(); i++) { for (unsigned i = 0; i < m_trail.size(); i++) {
out << dimacs_lit(m_trail[i]) << " 0\n"; out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n";
} }
vector<watch_list>::const_iterator it = m_watches.begin(); vector<watch_list>::const_iterator it = m_watches.begin();
vector<watch_list>::const_iterator end = m_watches.end(); vector<watch_list>::const_iterator end = m_watches.end();