mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

Retract changes in the commit 39a614559c. The fix was affecting benchmarks using the array theory map construct.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-04 08:19:33 -08:00
parent 39a614559c
commit 8e5581b4fe
3 changed files with 0 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/bv_decl_plugin.cpp
View file

@ -461,13 +461,6 @@ func_decl * bv_decl_plugin::mk_mkbv(unsigned arity, sort * const * domain) {
func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (range != 0) {
if (is_sort_of(range, m_family_id, BV_SORT))
m_manager->raise_exception("unneeded disambiguation");
else
m_manager->raise_exception("incorrect disambiguation");
return 0;
}
int bv_size;
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
// bv_size is filled in.
@ -566,13 +559,6 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) {
if (range != 0) {
if (is_sort_of(range, m_family_id, BV_SORT))
m_manager->raise_exception("unneeded disambiguation");
else
m_manager->raise_exception("incorrect disambiguation");
return 0;
}
int bv_size;
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
// bv_size is filled in.