mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

don't copy "true"

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-25 05:47:59 -07:00
parent 037c93b258
commit e75b5e9513
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.cpp
View file

@ -137,6 +137,8 @@ namespace smt {
for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) { for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) {
expr_ref fml(dst_m); expr_ref fml(dst_m);
proof_ref pr(dst_m); proof_ref pr(dst_m);
if (src_m.is_true(src_af.get_formula(i)))
continue;
proof* pr_src = src_af.get_formula_proof(i); proof* pr_src = src_af.get_formula_proof(i);
fml = tr(src_af.get_formula(i)); fml = tr(src_af.get_formula(i));
if (pr_src) { if (pr_src) {
@ -159,6 +161,8 @@ namespace smt {
} }
expr_ref fml0(src_m), fml1(dst_m); expr_ref fml0(src_m), fml1(dst_m);
src_ctx.literal2expr(lit, fml0); src_ctx.literal2expr(lit, fml0);
if (src_m.is_true(fml0))
continue;
fml1 = tr(fml0.get()); fml1 = tr(fml0.get());
dst_ctx.assert_expr(fml1); dst_ctx.assert_expr(fml1);
} }