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

Merge pull request #309 from NikolajBjorner/master

Browse source 
Fix for issue #308"
This commit is contained in:
Nikolaj Bjorner 2015-11-13 15:14:09 -05:00
commit 2277a52d80
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/opt/opt_context.cpp
View file

@ -770,7 +770,7 @@ namespace opt {
tout << "offset: " << offset << "\n"; tout << "offset: " << offset << "\n";
); );
std::ostringstream out; std::ostringstream out;
out << mk_pp(orig_term, m); out << mk_pp(orig_term, m) << ":" << index;
id = symbol(out.str().c_str()); id = symbol(out.str().c_str());
return true; return true;
} }
@ -793,7 +793,7 @@ namespace opt {
} }
neg = true; neg = true;
std::ostringstream out; std::ostringstream out;
out << mk_pp(orig_term, m); out << mk_pp(orig_term, m) << ":" << index;
id = symbol(out.str().c_str()); id = symbol(out.str().c_str());
return true; return true;
} }
@ -812,7 +812,7 @@ namespace opt {
} }
neg = is_max; neg = is_max;
std::ostringstream out; std::ostringstream out;
out << mk_pp(orig_term, m); out << mk_pp(orig_term, m) << ":" << index;
id = symbol(out.str().c_str()); id = symbol(out.str().c_str());
return true; return true;
} }