mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
remove unreferenced label
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6b28973799
commit
fff1426556
|
@ -1506,12 +1506,11 @@ lbool core::check(vector<lemma>& l_vec) {
|
||||||
m_tangents.tangent_lemma();
|
m_tangents.tangent_lemma();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
if (!m_reslim.inc())
|
if (!m_reslim.inc())
|
||||||
return l_undef;
|
return l_undef;
|
||||||
|
|
||||||
finish_up:
|
|
||||||
lbool ret = l_vec.empty() ? l_undef : l_false;
|
lbool ret = l_vec.empty() ? l_undef : l_false;
|
||||||
|
|
||||||
#if 0
|
#if 0
|
||||||
if (l_vec.empty())
|
if (l_vec.empty())
|
||||||
ret = m_nra.check();
|
ret = m_nra.check();
|
||||||
|
|
Loading…
Reference in a new issue