From bd0620f24538f8b9ee1fffbc2d8dc8cd4332cae8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 19:28:51 -0700 Subject: [PATCH] fix #3815 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_prob.cpp | 1 + src/sat/sat_types.h | 7 ++----- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_prob.cpp b/src/sat/sat_prob.cpp index 5bc2231ee..d0dcb2f60 100644 --- a/src/sat/sat_prob.cpp +++ b/src/sat/sat_prob.cpp @@ -123,6 +123,7 @@ namespace sat { } void prob::add(solver const& s) { + m_values.reserve(s.num_vars(), false); unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { add(1, s.m_trail.c_ptr() + i); diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index ceaeb819a..1991542bf 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -143,7 +143,7 @@ namespace sat { typedef svector model; inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); } - inline lbool value_at(bool_var v, model const & m) { return m[v]; } + inline lbool value_at(bool_var v, model const & m) { return m[v]; } inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; } inline std::ostream & operator<<(std::ostream & out, model const & m) { @@ -169,10 +169,7 @@ namespace sat { literal_set() {} literal_vector to_vector() const { literal_vector result; - iterator it = begin(), e = end(); - for (; it != e; ++it) { - result.push_back(*it); - } + for (literal lit : *this) result.push_back(lit); return result; } literal_set& operator=(literal_vector const& v) {