mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

duality fix

Browse source
This commit is contained in:
Ken McMillan 2014-03-21 10:35:33 -07:00
parent 3e91037a4d
commit fb2caf99e6
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/duality/duality_rpfp.cpp
View file

@ -150,8 +150,10 @@ namespace Duality {
}
return 0;
}
if(t.is_quantifier())
return CountOperatorsRec(memo,t.body())+2; // count 2 for a quantifier
if(t.is_quantifier()){
int nbv = t.get_quantifier_num_bound();
return CountOperatorsRec(memo,t.body()) + 2 * nbv; // count 2 for each quantifier
}
return 0;
}