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

merging duality and interpolation changes

Browse source
This commit is contained in:
Ken McMillan 2014-04-04 15:50:59 -07:00
parent bdc7bfde87 dee21c6656
commit 2b492f04f6
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_bv.cpp
View file

@ -117,6 +117,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_sort int_s = Z3_mk_int_sort(c);
if (is_signed) {
Z3_ast r = Z3_mk_bv2int(c, n, false);
Z3_inc_ref(c, r);
Z3_sort s = Z3_get_sort(c, n);
unsigned sz = Z3_get_bv_sort_size(c, s);
rational max_bound = power(rational(2), sz);
@ -135,6 +136,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_dec_ref(c, pred);
Z3_dec_ref(c, sub);
Z3_dec_ref(c, zero);
Z3_dec_ref(c, r);
RETURN_Z3(res);
}
else {

4
src/interp/iz3hash.h
View file

@ -464,7 +464,9 @@ namespace hash_space {
Value &operator[](const Key& key) {
std::pair<Key,Value> kvp(key,Value());
return lookup(kvp,true)->val.second;
return
hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>::
lookup(kvp,true)->val.second;
}
};