mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

another round of fix for #989 to avoid problems with doxygen generation (TravisCI build failure)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-27 12:59:34 -07:00
parent af47aa0120
commit ca67274519
2 changed files with 14 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

20
scripts/update_api.py
View file

@ -321,6 +321,7 @@ def mk_py_wrappers():
core_py.write("def %s(" % name) core_py.write("def %s(" % name)
display_args(num) display_args(num)
core_py.write("):\n") core_py.write("):\n")
core_py.write(" _lib = lib()\n")
core_py.write(" if _lib.%s is None:\n" % name) core_py.write(" if _lib.%s is None:\n" % name)
core_py.write(" return\n") core_py.write(" return\n")
if result != VOID: if result != VOID:
@ -1604,16 +1605,7 @@ def write_exe_c_preamble(exe_c):
def write_core_py_post(core_py): def write_core_py_post(core_py):
core_py.write(""" core_py.write("""
_dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
for _dir in _dirs:
try:
init(_dir)
break
except:
pass
if _lib is None:
raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
""") """)
def write_core_py_preamble(core_py): def write_core_py_preamble(core_py):
@ -1631,6 +1623,16 @@ _lib = None
def lib(): def lib():
global _lib global _lib
if _lib is None:
_dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
for _dir in _dirs:
try:
init(_dir)
break
except:
pass
if _lib is None:
raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
return _lib return _lib
def _to_ascii(s): def _to_ascii(s):

8
src/smt/theory_str.cpp
View file

@ -1549,14 +1549,12 @@ namespace smt {
expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m); expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m); expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
assert_axiom(breakdownAssert);
SASSERT(breakdownAssert); SASSERT(breakdownAssert);
expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m); expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
SASSERT(reduceToResult); assert_axiom(reduceToResult);
expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToResult), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
} }
void theory_str::instantiate_axiom_str_to_int(enode * e) { void theory_str::instantiate_axiom_str_to_int(enode * e) {