mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

ensure m_true is assigned #5753

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-11 10:41:54 -08:00
parent dbd5512d8c
commit e5eaea46aa
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/bv_internalize.cpp
View file

@ -371,6 +371,7 @@ namespace bv {
if (m_true == sat::null_literal) { if (m_true == sat::null_literal) {
ctx.push(value_trail<sat::literal>(m_true)); ctx.push(value_trail<sat::literal>(m_true));
m_true = ctx.internalize(m.mk_true(), false, true, false); m_true = ctx.internalize(m.mk_true(), false, true, false);
s().assign_unit(m_true);
} }
return m_true; return m_true;
} }