disable buggy code in slicer: it removes conjuncts for non-sliced variables. It should use the same criteria as the slice recognizer. reported by Arie Gurfinkel

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/muz_qe/dl_mk_slice.cpp

@@ -429,6 +429,33 @@ namespace datalog {
         }
     }
 
+    void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
+        expr_ref_vector conjs = get_tail_conjs(r);
+        for (unsigned j = 0; j < conjs.size(); ++j) {
+            expr* e = conjs[j].get();
+            expr_ref r(m);
+            unsigned v;
+            if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) {
+                TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";);
+                add_var(v);
+                if (!m_solved_vars[v].get()) { 
+                    add_free_vars(parameter_vars, r);
+                    m_solved_vars[v] = r;
+                }
+                else {
+                    // variables can only be solved once.
+                    add_free_vars(used_vars, e);
+                    add_free_vars(used_vars, m_solved_vars[v].get());
+                    used_vars.insert(v);
+                }
+            }
+            else {
+                add_free_vars(used_vars, e);
+            }
+        }
+    }
+
+
     bool mk_slice::prune_rule(rule& r) {
         TRACE("dl", r.display(m_ctx, tout << "prune:\n"); );
         bool change = false;
@@ -452,30 +479,8 @@ namespace datalog {
         // Collect the set of variables that are solved.
         // Collect the occurrence count of the variables per conjunct.
         // 
-        expr_ref_vector conjs = get_tail_conjs(r);
         uint_set used_vars, parameter_vars;
-        for (unsigned j = 0; j < conjs.size(); ++j) {
+        solve_vars(r, used_vars, parameter_vars);
-            expr* e = conjs[j].get();
-            expr_ref r(m);
-            unsigned v;
-            if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) {
-                TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";);
-                add_var(v);
-                if (!m_solved_vars[v].get()) { 
-                    add_free_vars(parameter_vars, r);
-                    m_solved_vars[v] = r;
-                }
-                else {
-                    // variables can only be solved once.
-                    add_free_vars(used_vars, e);
-                    add_free_vars(used_vars, m_solved_vars[v].get());
-                    used_vars.insert(v);
-                }
-            }
-            else {
-                add_free_vars(used_vars, e);
-            }
-        }
         uint_set::iterator it = used_vars.begin(), end = used_vars.end();
         for (; it != end; ++it) {     
             if (*it < m_var_is_sliceable.size()) {
@@ -725,9 +730,11 @@ namespace datalog {
         }
     }
 
+
     void mk_slice::update_rule(rule& r, rule_set& dst) {
         rule* new_rule;
         if (rule_updated(r)) {
+            init_vars(r);
             app_ref_vector tail(m);
             app_ref head(m);
             ptr_vector<sort> sorts;
@@ -742,10 +749,12 @@ namespace datalog {
             expr_ref_vector conjs = get_tail_conjs(r);
             
             m_solved_vars.reset();
+
+#if 0
             uint_set used_vars;
-            unsigned v;
             expr_ref b(m);
 
+        TBD: buggy code:
             for (unsigned i = 0; i < conjs.size(); ++i) {
                 expr* e = conjs[i].get();
                 if (is_eq(e, v, b)) {
@@ -772,15 +781,17 @@ namespace datalog {
                     add_free_vars(used_vars, e);
                 }
             }
+#endif
             for (unsigned i = 0; i < conjs.size(); ++i) {
                 expr* e = conjs[i].get();
-                if (is_eq(e, v, b) && m_solved_vars[v].get() && !used_vars.contains(v)) {
+#if 0
+                if (false && is_eq(e, v, b) && m_solved_vars[v].get() && !used_vars.contains(v)) {
                     TRACE("dl", tout << "removing conjunct: " << mk_pp(e, m) << "\n";);
                     // skip conjunct
                 }
-                else {
+#endif
-                    tail.push_back(to_app(e));
+                tail.push_back(to_app(e));
-                }
+                
             }
             
             new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0);        

src/muz_qe/dl_mk_slice.h

@@ -89,6 +89,8 @@ namespace datalog {
 
         void update_predicate(app* p, app_ref& q);
 
+        void solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars);
+
     public:
         /**
            \brief Create slice rule transformer for \c goal predicate. When applying the transformer,

src/muz_qe/horn_subsume_model_converter.cpp

@@ -195,7 +195,7 @@ void horn_subsume_model_converter::operator()(model_ref& mr) {
                 body = m.mk_or(e, body);
             }
             m_rewrite(body);
-            mr->register_decl(h, m.mk_or(e, body));
+            mr->register_decl(h, body);
         }
         else {
             func_interp* f = mr->get_func_interp(h);

src/muz_qe/pdr_util.cpp

@@ -916,6 +916,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
     class test_diff_logic {
         ast_manager& m;
         arith_util a;
+        bv_util    bv;
         bool m_is_dl;
 
         bool is_numeric(expr* e) const {
@@ -1017,14 +1018,21 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
                 return false;
             }
             family_id fid = to_app(e)->get_family_id();
+
+            if (fid == null_family_id && 
+                !m.is_bool(e) && 
+                to_app(e)->get_num_args() > 0) {
+                return true;
+            }
             return 
                 fid != m.get_basic_family_id() &&
                 fid != null_family_id &&
-                fid != a.get_family_id();
+                fid != a.get_family_id() &&
+                fid != bv.get_family_id();
         }
 
     public:
-        test_diff_logic(ast_manager& m): m(m), a(m), m_is_dl(true) {}
+        test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true) {}
         
         void operator()(expr* e) {
             if (!m_is_dl) {