mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

fix a few warnings

Browse source
This commit is contained in:
Ken McMillan 2014-01-28 11:43:00 -08:00
parent 466c35100d
commit 19830bcd33
3 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/cmd_context/interpolant_cmds.cpp
View file

@ -139,10 +139,11 @@ static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) {
get_interpolant_and_maybe_check(ctx,t,m_params,false); get_interpolant_and_maybe_check(ctx,t,m_params,false);
} }
#if 0
static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) { static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) {
get_interpolant_and_maybe_check(ctx,t,m_params,true); get_interpolant_and_maybe_check(ctx,t,m_params,true);
} }
#endif
static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){

2
src/duality/duality_rpfp.cpp
View file

@ -3661,7 +3661,7 @@ namespace Duality {
for(unsigned j = 0; j < outs.size(); j++) for(unsigned j = 0; j < outs.size(); j++)
for(unsigned k = 0; k < outs[j]->Children.size(); k++) for(unsigned k = 0; k < outs[j]->Children.size(); k++)
chs.push_back(outs[j]->Children[k]); chs.push_back(outs[j]->Children[k]);
Edge *fedge = CreateEdge(node,tr,chs); CreateEdge(node,tr,chs);
for(unsigned j = 0; j < outs.size(); j++) for(unsigned j = 0; j < outs.size(); j++)
edges_to_delete.insert(outs[j]); edges_to_delete.insert(outs[j]);
} }

2
src/interp/iz3translate_direct.cpp
View file

@ -58,7 +58,9 @@ namespace stl_ext {
static int lemma_count = 0; static int lemma_count = 0;
#if 0
static int nll_lemma_count = 0; static int nll_lemma_count = 0;
#endif
#define SHOW_LEMMA_COUNT -1 #define SHOW_LEMMA_COUNT -1
// One half of a resolution. We need this to distinguish // One half of a resolution. We need this to distinguish