mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix #2967

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-10 08:46:09 -08:00
parent a579ce1ea2
commit c36a980eb7
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/qe/qe_lite.cpp
View file

@ -37,7 +37,7 @@ Revision History:
#include "qe/qe_vartest.h" #include "qe/qe_vartest.h"
#include "qe/qe_solve_plugin.h" #include "qe/qe_solve_plugin.h"
namespace { namespace qel {
bool occurs_var(unsigned idx, expr* e) { bool occurs_var(unsigned idx, expr* e) {
if (is_ground(e)) return false; if (is_ground(e)) return false;
@ -616,6 +616,8 @@ namespace {
} }
bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) { bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) {
sort* s = m.get_sort(x);
if (!m.is_fully_interp(s) || !s->get_num_elements().is_infinite()) return false;
bool occ = occurs_var(x->get_idx(), t); bool occ = occurs_var(x->get_idx(), t);
for (unsigned j = 0; !occ && j < conjs.size(); ++j) { for (unsigned j = 0; !occ && j < conjs.size(); ++j) {
occ = (i != j) && occurs_var(x->get_idx(), conjs[j]); occ = (i != j) && occurs_var(x->get_idx(), conjs[j]);
@ -2259,9 +2261,9 @@ class qe_lite::impl {
private: private:
ast_manager& m; ast_manager& m;
eq_der m_der; qel::eq_der m_der;
fm::fm m_fm; qel::fm::fm m_fm;
ar_der m_array_der; qel::ar_der m_array_der;
elim_star m_elim_star; elim_star m_elim_star;
th_rewriter m_rewriter; th_rewriter m_rewriter;