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

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-28 12:06:14 -08:00
parent 3e191d5cc5
commit 2f6c80ef08
1 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/sat_model_converter.cpp
View file

@ -43,10 +43,7 @@ namespace sat {
// and the following procedure flips its value. // and the following procedure flips its value.
bool sat = false; bool sat = false;
bool var_sign = false; bool var_sign = false;
literal_vector::const_iterator it2 = it->m_clauses.begin(); for (literal l : it->m_clauses) {
literal_vector::const_iterator end2 = it->m_clauses.end();
for (; it2 != end2; ++it2) {
literal l = *it2;
if (l == null_literal) { if (l == null_literal) {
// end of clause // end of clause
if (!sat) { if (!sat) {
@ -74,7 +71,7 @@ namespace sat {
DEBUG_CODE({ DEBUG_CODE({
// all clauses must be satisfied // all clauses must be satisfied
bool sat = false; bool sat = false;
for (literal l : m_clauses) { for (literal l : it->m_clauses) {
if (l == null_literal) { if (l == null_literal) {
SASSERT(sat); SASSERT(sat);
sat = false; sat = false;