mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

fix more compiler warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-03 17:11:33 -07:00
parent 282173773f
commit 65dff93e93
2 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -1015,7 +1015,6 @@ namespace datalog {
virtual void operator()(relation_base & _r) {
karr_relation & r = get(_r);
karr_relation_plugin & p = r.get_plugin();
if (m_value.is_int()) {
r.get_ineqs();
vector<rational> row;

7
src/muz_qe/fdd.cpp
View file

@ -42,11 +42,11 @@ bool node::operator==(node const& other) const {
// ------------------------------------------
// manager
manager::manager() :
manager::manager() :
m_alloc_node(2),
m_false(0),
m_true(1),
m_root(m_false),
m_alloc_node(2)
m_root(m_false)
{
m_nodes.push_back(node()); // false
m_nodes.push_back(node()); // true
@ -183,7 +183,6 @@ node_id manager::insert(unsigned idx, node_id n) {
node nd = m_nodes[n];
SASSERT(idx >= nd.var());
unsigned idx0 = idx;
while (idx > nd.var()) {
if (idx2bit(idx) && !is_dont_care(idx2key(idx))) {
return mk_node(idx, n, insert(idx, n));