From 2475f3bff59a0e15fbc9560e0896856f817faf87 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Oct 2016 07:41:27 -0700 Subject: [PATCH] ensure that variables passed to consequence finding have bound constraints, if applicable. Even if those variables do not occur in the constraints Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/enum2bv_solver.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index b0f11cb91..e89f9d188 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -102,9 +102,20 @@ public: datatype_util dt(m); bv_util bv(m); + expr_ref_vector bvars(m), conseq(m), bounds(m); + + // ensure that enumeration variables that + // don't occur in the constraints + // are also internalized. + for (unsigned i = 0; i < vars.size(); ++i) { + expr_ref tmp(m.mk_eq(vars[i], vars[i]), m); + proof_ref proof(m); + m_rewriter(tmp, tmp, proof); + } + m_rewriter.flush_side_constraints(bounds); + m_solver->assert_expr(bounds); // translate enumeration constants to bit-vectors. - expr_ref_vector bvars(m), conseq(m); for (unsigned i = 0; i < vars.size(); ++i) { func_decl* f; if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {