mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

update to c++20, remove debug output

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-09-22 21:30:44 +01:00
parent 96c1375786
commit 1e580a7f12
3 changed files with 7 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/converters/generic_model_converter.cpp
View file

@ -156,7 +156,6 @@ void generic_model_converter::convert_initialize_value(expr* def, unsigned i, ve
// el = value => c = false
expr* c = nullptr, *th = nullptr, *el = nullptr;
auto& [var, value] = var2value[i];
verbose_stream() << "def " << mk_pp(def, m) << "\n";
if (m.is_ite(def, c, th, el)) {
if (value == th) {
var = c;
@ -175,13 +174,7 @@ void generic_model_converter::convert_initialize_value(expr* def, unsigned i, ve
if (is_uninterp(def)) {
var = def;
return;
}
bv_util bv(m);
if (bv.is_mkbv(def)) {
verbose_stream() << "def\n";
}
}
}