diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-09 15:51:26 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-09 15:51:26 +0200 |
| commit | 3f59801357808a538934b04ce7bf0894dec1b0dd (patch) | |
| tree | 9a32729a077f25fbd7ef2e84825d1e177d29bafd /src/theory/quantifiers/conjecture_generator.cpp | |
| parent | 7443276e61db276e5ba48d605cb6b08a35c5a100 (diff) | |
Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing. Minor fix for conjecture generation for finite types.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
| -rwxr-xr-x | src/theory/quantifiers/conjecture_generator.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 48d3f3902..116debb7c 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1159,6 +1159,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< vec[i] = 0;
}
vec_sum = -1;
+ }else{
+ return;
}
}
}
|