mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
a0503ba6a1
|
@ -3650,10 +3650,15 @@ class MakeRuleCmd(object):
|
|||
assert not ' ' in dir
|
||||
install_root = cls._install_root(dir, in_prefix, out)
|
||||
|
||||
cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
|
||||
install_root=install_root,
|
||||
dir=dir))
|
||||
|
||||
if is_windows():
|
||||
cls.write_cmd(out, "IF NOT EXIST {dir} (mkdir {dir})".format(
|
||||
install_root=install_root,
|
||||
dir=dir))
|
||||
else:
|
||||
cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
|
||||
install_root=install_root,
|
||||
dir=dir))
|
||||
|
||||
@classmethod
|
||||
def _is_path_prefix_of(cls, temp_path, target_as_abs):
|
||||
"""
|
||||
|
|
|
@ -935,7 +935,6 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
|
||||
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
|
||||
|
@ -1037,7 +1036,6 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||
SASSERT(plugin != 0);
|
||||
|
|
|
@ -634,9 +634,6 @@ struct app_flags {
|
|||
unsigned m_ground:1; // application does not have free variables or nested quantifiers.
|
||||
unsigned m_has_quantifiers:1; // application has nested quantifiers.
|
||||
unsigned m_has_labels:1; // application has nested labels.
|
||||
static app_flags mk_const_flags();
|
||||
static app_flags mk_default_app_flags();
|
||||
static app_flags mk_default_quantifier_flags();
|
||||
};
|
||||
|
||||
class app : public expr {
|
||||
|
|
Loading…
Reference in a new issue