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

src/interp/iz3mgr.cpp

@@ -33,9 +33,11 @@
 #include <fstream>
 #include <iostream>
 #include <ostream>
+#include <sstream>
 
 #include "ast/expr_abstract.h"
 #include "util/params.h"
+#include "ast/used_vars.h"
 
 
 using namespace stl_ext;
@@ -938,3 +940,30 @@ void iz3mgr::get_bound_substitutes(stl_ext::hash_map<ast,bool> &memo, const ast
  
     }
 #endif
+
+unsigned  iz3mgr::num_free_variables(const ast &e){
+    used_vars uv;
+    uv(to_expr(e.raw()));
+    return uv.get_num_vars();
+}
+
+iz3mgr::ast iz3mgr::close_universally (ast e){
+   used_vars uv;
+   uv(to_expr(e.raw()));
+   std::vector<ast> bvs;
+   stl_ext::hash_map<ast,ast> subst_memo;
+   for (unsigned i = 0; i < uv.get_max_found_var_idx_plus_1(); i++){
+       if (uv.get(i)) {
+           std::ostringstream os;
+           os << "%%" << i;
+           ast c = make_var(os.str(),uv.get(i));
+           ast v = cook(m().mk_var(i,uv.get(i)));
+           subst_memo[v] = c;
+           bvs.push_back(c);
+       }
+   }
+   e = subst(subst_memo,e);
+   for (unsigned i = 0; i < bvs.size(); i++)
+       e = apply_quant(Forall,bvs[i],e);
+   return e;
+}

src/interp/iz3mgr.h

@@ -661,6 +661,12 @@ class iz3mgr  {
 
     ast apply_quant(opr quantifier, ast var, ast e);
 
+    // Universally quantify all the free variables in a formula.
+    // Makes up names for the quntifiers.
+
+    ast close_universally (ast e);
+
+    unsigned num_free_variables(const ast &e);
 
     /** For debugging */
     void show(ast);

src/interp/iz3proof_itp.cpp

@@ -2968,9 +2968,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast interpolate(const node &pf){
         // proof of false must be a formula, with quantified symbols
 #ifndef BOGUS_QUANTS
-        return add_quants(z3_simplify(pf));
+        return close_universally(add_quants(z3_simplify(pf)));
 #else
-        return z3_simplify(pf);
+        return close_universally(z3_simplify(pf));
 #endif
     }
 

src/interp/iz3translate.cpp

@@ -234,6 +234,11 @@ public:
                 }
             }
 
+            // if(!range_is_empty(rng)){
+            //     if (num_free_variables(con) > 0)
+            //         rng = range_empty();
+            // }
+
             if(res == INT_MAX){
                 if(range_is_empty(rng))
                     res = -1;