mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Fix build (#4960)

Browse source
This commit is contained in:
Artem Alekseev 2021-01-23 22:13:10 +03:00 • committed by GitHub
parent 03fd251ccb
commit 7e668e9a1f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/seq_unicode.cpp
View file

@ -89,7 +89,7 @@ namespace smt {
for (literal bit : bits) for (literal bit : bits)
ctx().mark_as_relevant(bit); ctx().mark_as_relevant(bit);
expr_ref bits2char(seq.mk_skolem(m_bits2char, ebits.size(), ebits.c_ptr(), m.get_sort(e)), m); expr_ref bits2char(seq.mk_skolem(m_bits2char, ebits.size(), ebits.c_ptr(), m.get_sort(e)), m);
ctx().mark_as_relevant(bits2char); ctx().mark_as_relevant(bits2char.get());
enode* n1 = th.ensure_enode(e); enode* n1 = th.ensure_enode(e);
enode* n2 = th.ensure_enode(bits2char); enode* n2 = th.ensure_enode(bits2char);
justification* j = justification* j =