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

enable coercions when interpolation creates MILP constraints. Issue #217

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-09-12 14:47:35 +02:00
parent d7da64f946
commit a8b47b4fb2
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/interp/iz3translate.cpp
View file

@ -1407,6 +1407,7 @@ public:
hash_map<ast,ast> dual_map; hash_map<ast,ast> dual_map;
std::vector<ast> cvec, vars_seen; std::vector<ast> cvec, vars_seen;
m().enable_int_real_coercions(true);
ast rhs = make_real(rational(0)); ast rhs = make_real(rational(0));
for(unsigned i = 0; i < npcons.size(); i++){ for(unsigned i = 0; i < npcons.size(); i++){
ast c= mk_fresh_constant("@c",real_type()); ast c= mk_fresh_constant("@c",real_type());