From 7d35fcb17eb035ebd1b63ff3d62c7a4101fe7435 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 5 Apr 2017 19:42:02 +0100 Subject: [PATCH] Avoid null pointer warnings in justifications. --- src/smt/smt_justification.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index c091f6973..7a9938cd0 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -246,13 +246,15 @@ namespace smt { simple_justification::simple_justification(region & r, unsigned num_lits, literal const * lits): m_num_literals(num_lits) { - m_literals = new (r) literal[num_lits]; - memcpy(m_literals, lits, sizeof(literal) * num_lits); + if (num_lits != 0) { + m_literals = new (r) literal[num_lits]; + memcpy(m_literals, lits, sizeof(literal) * num_lits); #ifdef Z3DEBUG - for (unsigned i = 0; i < num_lits; i++) { - SASSERT(lits[i] != null_literal); - } + for (unsigned i = 0; i < num_lits; i++) { + SASSERT(lits[i] != null_literal); + } #endif + } } void simple_justification::get_antecedents(conflict_resolution & cr) {