From c8a67abdd70550cbab22bafd259a21f68433da7c Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Mon, 25 Sep 2017 14:33:20 -0700
Subject: [PATCH] fixing issue [1269]

---
 src/interp/iz3mgr.cpp       | 29 +++++++++++++++++++++++++++++
 src/interp/iz3mgr.h         |  6 ++++++
 src/interp/iz3proof_itp.cpp |  4 ++--
 src/interp/iz3translate.cpp |  5 +++++
 4 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index 306807f1f..7314403b0 100755
--- a/src/interp/iz3mgr.cpp
+++ b/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;
+}
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index e6e08f84d..6ca8fae34 100755
--- a/src/interp/iz3mgr.h
+++ b/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);
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index eb7f8e325..fc9d0fac6 100755
--- a/src/interp/iz3proof_itp.cpp
+++ b/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
     }
 
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index ebbee46ca..c59dd0178 100755
--- a/src/interp/iz3translate.cpp
+++ b/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;