mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +00:00
Code Activity

fix overflow and integrality bugs reported by Phan

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-12-15 16:19:38 -08:00
parent ae3d16bc50
commit 1d18934ddb
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/muz/rel/dl_mk_explanations.cpp
View file

@ -434,7 +434,6 @@ namespace datalog {
relation_union_fn * explanation_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src, relation_union_fn * explanation_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src,
const relation_base * delta) { const relation_base * delta) {
std::cout << "check kind: " << check_kind(tgt) << "\n";
if (!check_kind(tgt) || (delta && !check_kind(*delta))) { if (!check_kind(tgt) || (delta && !check_kind(*delta))) {
return 0; return 0;
} }