mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix-eq bits and projection

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-18 14:08:53 -07:00
parent c2db127a45
commit 4173bf930b
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/muz/ddnf/doc.cpp
View file

@ -334,6 +334,7 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
(*t1).set(i, BIT_x);
for (unsigned k = 0; k < neg.size(); ++k) {
if (tbvm().set_and(*t1, *neg[k])) {
(*t1).set(i, BIT_x);
new_todo.push_back(t1.detach());
t1 = tbvm().allocate(*pos[j]);
(*t1).set(i, BIT_x);