mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #5907

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-03-20 11:40:19 -07:00
parent f053daa051
commit b4873d226c
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_datatype.cpp
View file

@ -254,6 +254,8 @@ namespace smt {
app_ref n_is_con(m.mk_app(rec, own), m); app_ref n_is_con(m.mk_app(rec, own), m);
ctx.internalize(n_is_con, false); ctx.internalize(n_is_con, false);
literal lits[2] = { ~is_con, literal(ctx.get_bool_var(n_is_con)) }; literal lits[2] = { ~is_con, literal(ctx.get_bool_var(n_is_con)) };
ctx.mark_as_relevant(lits[0]);
ctx.mark_as_relevant(lits[1]);
std::function<literal_vector(void)> fn = [&]() { return literal_vector(2, lits); }; std::function<literal_vector(void)> fn = [&]() { return literal_vector(2, lits); };
scoped_trace_stream _st(*this, fn); scoped_trace_stream _st(*this, fn);
ctx.mk_th_axiom(get_id(), 2, lits); ctx.mk_th_axiom(get_id(), 2, lits);