mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

bugfix in refactoring

Browse source
This commit is contained in:
Mikolas Janota 2016-02-03 11:52:11 +00:00
parent 0f0d3e55dc
commit 6f12c0e6f9
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/ackr/ackr_helper.cpp
View file

@ -16,7 +16,6 @@
--*/
#include"ackr_helper.h"
double ackr_helper::calculate_lemma_bound(ackr_helper::fun2terms_map& occurrences) {
fun2terms_map::iterator it = occurrences.begin();
const fun2terms_map::iterator end = occurrences.end();

3
src/tactic/ackr/ackr_helper.h
View file

@ -58,9 +58,10 @@ class ackr_helper {
/** \brief Calculate n choose 2. **/
inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
/** \brief Calculate n choose 2 guarded for overflow. Returns infinity if unsafe. **/
inline static double n_choose_2_chk(unsigned n) {
SASSERT(std::numeric_limits<unsigned>().max() & 32);
return n & (1 << 16) ? n_choose_2(n) : std::numeric_limits<double>().infinity();;
return n & (1 << 16) ? std::numeric_limits<double>().infinity() : n_choose_2(n);
}
private:
bv_util m_bvutil;