mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-08 15:38:13 -07:00
parent af700e88cf
commit 30df2837fb
4 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_boogie_proof.cpp
View file

@ -176,7 +176,7 @@ namespace datalog {
step &s = steps[j];
// TBD
s.m_labels;
// s.m_labels;
// set references, compensate for reverse ordering.
for (unsigned i = 0; i < s.m_refs.size(); ++i) {

1
src/muz_qe/dl_compiler.cpp
View file

@ -1004,7 +1004,6 @@ namespace datalog {
void compiler::detect_chains(const func_decl_set & preds, func_decl_vector & ordered_preds,
func_decl_set & global_deltas) {
typedef obj_map<func_decl, func_decl *> pred2pred;
SASSERT(ordered_preds.empty());
SASSERT(global_deltas.empty());

3
src/muz_qe/dl_context.cpp
View file

@ -686,6 +686,7 @@ namespace datalog {
check_existential_tail(r);
check_positive_predicates(r);
break;
case LAST_ENGINE:
default:
UNREACHABLE();
break;
@ -1039,6 +1040,8 @@ namespace datalog {
case CLP_ENGINE:
m_engine = alloc(clp, *this);
break;
case LAST_ENGINE:
UNREACHABLE();
}
}
}

1
src/muz_qe/dl_mk_array_blast.cpp
View file

@ -107,7 +107,6 @@ namespace datalog {
m_next_var = 0;
ptr_vector<expr> todo;
todo.push_back(head);
unsigned next_var = 0;
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
expr* x, *y;