cvc4/cvc4-vec.patch
2018-07-10 21:22:52 -06:00

25 lines
1000 B
Diff

--- src/theory/quantifiers/conjecture_generator.cpp.orig 2018-06-25 15:13:18.823929253 -0600
+++ src/theory/quantifiers/conjecture_generator.cpp 2018-07-07 14:37:50.162382038 -0600
@@ -1089,16 +1089,17 @@ void ConjectureGenerator::getEnumerateUf
vec_sum = 0;
vec.push_back( size_limit );
}else{
+ int vecindex = (index < vec.size()) ? vec[index] : 0;
//see if we can iterate current
if (vec_sum < size_limit
- && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull())
+ && !te->getEnumerateTerm(types[index], vecindex + 1).isNull())
{
- vec[index]++;
+ vec.assign(index, vecindex + 1);
vec_sum++;
vec.push_back( size_limit - vec_sum );
}else{
- vec_sum -= vec[index];
- vec[index] = 0;
+ vec_sum -= vecindex;
+ vec.assign(index, 0);
index++;
if( index==n.getNumChildren() ){
success = false;