projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
cc72711
)
minor fix for merge
author
Tianyi Liang
<tianyi-liang@uiowa.edu>
Wed, 5 Feb 2014 15:19:23 +0000
(09:19 -0600)
committer
Tianyi Liang
<tianyi-liang@uiowa.edu>
Tue, 11 Feb 2014 22:41:33 +0000
(16:41 -0600)
src/theory/strings/theory_strings.cpp
patch
|
blob
|
history
diff --git
a/src/theory/strings/theory_strings.cpp
b/src/theory/strings/theory_strings.cpp
index 00688a95d2179422e314a8c5f88d7134ac049d00..43132b324fb85ef2e876ed9f9ddedb05f5152a24 100644
(file)
--- a/
src/theory/strings/theory_strings.cpp
+++ b/
src/theory/strings/theory_strings.cpp
@@
-2051,7
+2051,7
@@
bool TheoryStrings::checkCardinality() {
Node lr = lts[i];
Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
// size > c^k
- double k =
std::log( cols[i].size() ) / log((double) cardinality
);
+ double k =
cols[i].size() < cardinality? 0.0 : ( std::log( cols[i].size() ) / log((double) cardinality)
);
unsigned int int_k = (unsigned int) k;
//double c_k = pow ( (double)cardinality, (double)lr );
if( cols[i].size() > 1 ) {