mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

use-before-def

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-06 16:41:13 -08:00
parent 2999d33ede
commit 88fc4c82aa
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/bv_decl_plugin.cpp
View file

@ -853,10 +853,10 @@ bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational
} }
bv_util::bv_util(ast_manager & m): bv_util::bv_util(ast_manager & m):
bv_recognizers(m.mk_family_id(m_plugin->m_bv_sym)), bv_recognizers(m.mk_family_id(symbol("bv"))),
m_manager(m) { m_manager(m) {
SASSERT(m.has_plugin(m_plugin->m_bv_sym));
m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv"))); m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv")));
SASSERT(m.has_plugin(symbol("bv")));
} }
app * bv_util::mk_numeral(rational const & val, sort* s) const { app * bv_util::mk_numeral(rational const & val, sort* s) const {