From 64103038a7528b0b2c1c37a14fdc5dd72666068a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Dec 2018 12:20:53 +0800 Subject: [PATCH] simplify Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbi.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index f7c50e4c9..61d6c5ff4 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -350,7 +350,7 @@ namespace qe { // 1. arithmetical variables - atomic and in purified positions app_ref_vector avars = get_arith_vars(mdl, lits); - TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";); + TRACE("qe", tout << "vars: " << avars << "\nlits: " << lits << "\n";); // 2. project private non-arithmetical variables from lits project_euf(mdl, lits, avars); @@ -371,7 +371,7 @@ namespace qe { } /** - * \brief subistute solution to arithmetical variables into lits + * \brief substitute solution to arithmetical variables into lits */ void euf_arith_mbi_plugin::substitute(vector const& defs, expr_ref_vector& lits) { for (auto const& def : defs) {