summaryrefslogtreecommitdiff
path: root/src/main/main.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-09-21 21:51:25 +0000
committerMorgan Deters <mdeters@gmail.com>2010-09-21 21:51:25 +0000
commit2b2d9092eea1f50b468e459029dcfdd88e2232da (patch)
tree82de73997d5e7193fb32d730cdfa00719b95052b /src/main/main.cpp
parent9dbc683d057288a23109075d806a5398252eaa12 (diff)
fix statistics-registry-related memory leaks
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r--src/main/main.cpp9
1 files changed, 5 insertions, 4 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 235ebb354..a6fe10888 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -188,8 +188,6 @@ int runCvc4(int argc, char* argv[]) {
}
Result asSatResult = lastResult.asSatisfiabilityResult();
-
-
int returnValue;
switch(asSatResult.isSAT()) {
@@ -216,15 +214,18 @@ int runCvc4(int argc, char* argv[]) {
// Remove the parser
delete parser;
-ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult);
+
+ ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult);
StatisticsRegistry::registerStat(&s_statSatResult);
if(options.statistics){
StatisticsRegistry::flushStatistics(cerr);
}
- return returnValue;
+ StatisticsRegistry::unregisterStat(&s_statSatResult);
+ StatisticsRegistry::unregisterStat(&s_statFilename);
+ return returnValue;
}
void doCommand(SmtEngine& smt, Command* cmd) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback