mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-10-25 20:32:20 -07:00
commit d0c5b86a2a
3 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_util.py
View file

@ -1505,6 +1505,9 @@ class PythonInstallComponent(Component):
os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'), os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'),
in_prefix=self.in_prefix_install in_prefix=self.in_prefix_install
) )
MakeRuleCmd.remove_installed_files(out,
os.path.join(self.pythonPkgDir, 'z3', 'lib',
self.libz3Component.dll_file()))
def mk_makefile(self, out): def mk_makefile(self, out):
return return

2
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -224,12 +224,12 @@ struct pb2bv_rewriter::imp {
public: public:
card2bv_rewriter(imp& i, ast_manager& m): card2bv_rewriter(imp& i, ast_manager& m):
m_sort(*this),
m(m), m(m),
m_imp(i), m_imp(i),
au(m), au(m),
pb(m), pb(m),
bv(m), bv(m),
m_sort(*this),
m_trail(m), m_trail(m),
m_args(m) m_args(m)
{} {}

3
src/test/qe_arith.cpp
View file

@ -375,6 +375,9 @@ static void add_random_ineq(
case opt::t_le: case opt::t_le:
fml = a.mk_le(t1, t2); fml = a.mk_le(t1, t2);
break; break;
case opt::t_mod:
NOT_IMPLEMENTED_YET();
break;
} }
fmls.push_back(fml); fmls.push_back(fml);
mbo.add_constraint(vars, rational(coeff), rel); mbo.add_constraint(vars, rational(coeff), rel);