diff --git a/src/api/dotnet/Deprecated.cs b/src/api/dotnet/Deprecated.cs index 7282796ec..7dc524834 100644 --- a/src/api/dotnet/Deprecated.cs +++ b/src/api/dotnet/Deprecated.cs @@ -94,7 +94,6 @@ namespace Microsoft.Z3 /// /// Retrieves an assignment to atomic propositions for a satisfiable context. /// - /// public static BoolExpr GetAssignment(Context ctx) { IntPtr x = Native.Z3_get_context_assignment(ctx.nCtx); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 86c0efb8f..be39a05d5 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -356,9 +356,9 @@ public: while (index < asms.size() && is_sat == l_true) { while (asms.size() > 20*(index - last_index) && index < asms.size()) { index = next_index(asms, index); - //std::cout << "weight: " << get_weight(asms[index-1].get()) << "\n"; //break; } + IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << "\n";); last_index = index; is_sat = s().check_sat(index, asms.c_ptr()); } diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index dd77db9f8..31908a41d 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -146,6 +146,8 @@ public: test_filter_neg4(false); test_filter_neg4(true); + test_filter_neg6(false); + test_filter_neg6(true); test_filter_neg(); test_filter_neg2(); @@ -658,6 +660,35 @@ public: neg->deallocate(); } + void test_filter_neg5(bool disable_fast) { + relation_signature sig1, sig2; + sig1.push_back(bv.mk_sort(2)); + sig1.push_back(bv.mk_sort(2)); + sig2.push_back(bv.mk_sort(2)); + sig2.push_back(bv.mk_sort(2)); + sig2.push_back(bv.mk_sort(2)); + unsigned_vector cols1, cols2, cols3; + + cols1.push_back(0); + cols1.push_back(1); + cols2.push_back(0); + cols2.push_back(2); + cols3.push_back(0); + cols3.push_back(1); + cols3.push_back(2); + udoc_relation* tgt = mk_full(sig1); + udoc_relation* neg = mk_full(sig2); + rel_mut filter_id = p.mk_filter_identical_fn(*tgt, cols3.size(), cols3.c_ptr()); + (*filter_id)(*tgt); + if (disable_fast) p.disable_fast_pass(); + apply_filter_neg(*tgt, *neg, cols1, cols2); + tgt->deallocate(); + neg->deallocate(); + } + + // TBD: unit test to expose similar bug as projection had. + // you can't just remove columns when there are side-constraints in neg. + void set_random(udoc_relation& r, unsigned num_vals) { unsigned num_bits = r.get_dm().num_tbits(); udoc_relation* full = mk_full(r.get_signature());