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

fix bug in getting decision count in duality

Browse source
This commit is contained in:
Ken McMillan 2013-05-31 17:52:51 -07:00
parent dfae0c5109
commit ca38158966
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/duality/duality_wrapper.cpp
View file

@ -296,6 +296,7 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
st.display(ss);
std::string stats = ss.str();
int pos = stats.find("decisions:");
if(pos < 0) return 0; // for some reason, decisions are not reported if there are none
pos += 10;
int end = stats.find('\n',pos);
std::string val = stats.substr(pos,end-pos);