mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
Merge pull request #742 from angr/fix-tests
Fix z3test for build rearrangement
This commit is contained in:
commit
9746794962
|
@ -2779,6 +2779,8 @@ def cp_z3py_to_build():
|
||||||
shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
|
shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
|
||||||
if is_verbose():
|
if is_verbose():
|
||||||
print("Copied '%s'" % pyc)
|
print("Copied '%s'" % pyc)
|
||||||
|
# Copy z3test.py
|
||||||
|
shutil.copyfile(os.path.join(Z3PY_SRC_DIR, 'z3test.py'), os.path.join(BUILD_DIR, 'python', 'z3test.py'))
|
||||||
|
|
||||||
def mk_bindings(api_files):
|
def mk_bindings(api_files):
|
||||||
if not ONLY_MAKEFILES:
|
if not ONLY_MAKEFILES:
|
||||||
|
|
|
@ -148,7 +148,7 @@ setup(
|
||||||
packages=['z3'],
|
packages=['z3'],
|
||||||
include_package_data=True,
|
include_package_data=True,
|
||||||
package_data={
|
package_data={
|
||||||
'z3': [os.path.join('lib', '*'), os.path.join('include', '*')]
|
'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]
|
||||||
},
|
},
|
||||||
scripts=[os.path.join('bin', 'z3')],
|
scripts=[os.path.join('bin', 'z3')],
|
||||||
cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg},
|
cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg},
|
||||||
|
|
|
@ -41,6 +41,7 @@ Z3 exceptions:
|
||||||
... print("failed: %s" % ex)
|
... print("failed: %s" % ex)
|
||||||
failed: sort mismatch
|
failed: sort mismatch
|
||||||
"""
|
"""
|
||||||
|
from . import z3core
|
||||||
from .z3core import *
|
from .z3core import *
|
||||||
from .z3types import *
|
from .z3types import *
|
||||||
from .z3consts import *
|
from .z3consts import *
|
||||||
|
|
|
@ -572,9 +572,4 @@ def isolate_roots(p, vs=[]):
|
||||||
_vs[i] = vs[i].ast
|
_vs[i] = vs[i].ast
|
||||||
_roots = AstVector(Z3_algebraic_roots(p.ctx_ref(), p.as_ast(), num, _vs), p.ctx)
|
_roots = AstVector(Z3_algebraic_roots(p.ctx_ref(), p.as_ast(), num, _vs), p.ctx)
|
||||||
return [ Numeral(r) for r in _roots ]
|
return [ Numeral(r) for r in _roots ]
|
||||||
|
|
||||||
if __name__ == "__main__":
|
|
||||||
import doctest
|
|
||||||
if doctest.testmod().failed:
|
|
||||||
exit(1)
|
|
||||||
|
|
||||||
|
|
|
@ -5,9 +5,16 @@
|
||||||
#
|
#
|
||||||
# Author: Leonardo de Moura (leonardo)
|
# Author: Leonardo de Moura (leonardo)
|
||||||
############################################
|
############################################
|
||||||
import z3, doctest
|
import z3, doctest, sys
|
||||||
|
|
||||||
|
if len(sys.argv) < 2 or sys.argv[1] == 'z3':
|
||||||
|
r = doctest.testmod(z3.z3)
|
||||||
|
elif sys.argv[1] == 'z3num':
|
||||||
|
r = doctest.testmod(z3.z3num)
|
||||||
|
else:
|
||||||
|
print 'Usage: z3test.py (z3 | z3num)'
|
||||||
|
sys.exit(1)
|
||||||
|
|
||||||
r = doctest.testmod(z3)
|
|
||||||
if r.failed != 0:
|
if r.failed != 0:
|
||||||
exit(1)
|
sys.exit(1)
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue