mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

simplify

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-12-28 12:20:53 +08:00
parent 0628711c4a
commit 64103038a7
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/qe/qe_mbi.cpp
View file

@ -350,7 +350,7 @@ namespace qe {
// 1. arithmetical variables - atomic and in purified positions // 1. arithmetical variables - atomic and in purified positions
app_ref_vector avars = get_arith_vars(mdl, lits); 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 // 2. project private non-arithmetical variables from lits
project_euf(mdl, lits, avars); 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<def> const& defs, expr_ref_vector& lits) { void euf_arith_mbi_plugin::substitute(vector<def> const& defs, expr_ref_vector& lits) {
for (auto const& def : defs) { for (auto const& def : defs) {