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

minor fixes for OSX

Browse source
This commit is contained in:
Kenneth McMillan 2013-03-04 19:53:46 -08:00
parent e5f5e008aa
commit 12d2d3beef
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/interp/iz3foci.cpp
View file

@ -73,9 +73,9 @@ public:
// create a symbol corresponding to a DeBruijn index of a particular type // create a symbol corresponding to a DeBruijn index of a particular type
// the type has to be encoded into the name because the same index can // the type has to be encoded into the name because the same index can
// occur with different types // occur with different types
foci2::symb make_deBruijn_symbol(int index, int type){ foci2::symb make_deBruijn_symbol(int index, type ty){
std::ostringstream s; std::ostringstream s;
s << "#" << index << "#" << type; // s << "#" << index << "#" << type;
return foci->mk_func(s.str()); return foci->mk_func(s.str());
} }
@ -181,7 +181,7 @@ public:
case Variable: { // a deBruijn index case Variable: { // a deBruijn index
int index = get_variable_index_value(t); int index = get_variable_index_value(t);
type ty = get_type(t); type ty = get_type(t);
foci2::symb symbol = make_deBruijn_symbol(index,(int)(ty)); foci2::symb symbol = make_deBruijn_symbol(index,ty);
res = foci->mk_app(symbol,std::vector<foci2::ast>()); res = foci->mk_app(symbol,std::vector<foci2::ast>());
} }
default: default:

4
src/interp/iz3mgr.cpp
View file

@ -264,8 +264,8 @@ void iz3mgr::pretty_print(std::ostream &f, const std::string &s){
col = indent; col = indent;
continue; continue;
} }
unsigned paren = s.find('(',pos); int paren = s.find('(',pos);
if(paren != std::string::npos){ if(paren != (int)std::string::npos){
int chars = paren - pos + 1; int chars = paren - pos + 1;
f << s.substr(pos,chars); f << s.substr(pos,chars);
indent += pretty_indent_chars; indent += pretty_indent_chars;