From 44b0b0148b949c43ce5e3c7917d9c791f87f815c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 17:13:32 -0700 Subject: [PATCH] deal with warnings Signed-off-by: Nikolaj Bjorner --- src/sat/sat_drat.cpp | 2 +- src/smt/asserted_formulas.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 5de340674..16785d566 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -100,7 +100,7 @@ namespace sat { v /= 10; SASSERT(d > digits); } - SASSERT(len + lastd - d < sizeof(buffer)); + SASSERT(len + lastd < sizeof(buffer) + d); memcpy(buffer + len, d, lastd - d); len += static_cast(lastd - d); buffer[len++] = ' '; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index b1e89f72e..d44548f0b 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -439,6 +439,7 @@ void asserted_formulas::commit(unsigned new_qhead) { justified_expr const& j = m_formulas[i]; update_substitution(j.get_fml(), j.get_proof()); } + (void)new_sub; m_qhead = new_qhead; }