summaryrefslogtreecommitdiff
path: root/src/main/driver_unified.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r--src/main/driver_unified.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index c110ffa4f..71f47906d 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -28,7 +28,6 @@
#include "base/output.h"
#include "expr/expr_iomanip.h"
#include "expr/expr_manager.h"
-#include "expr/statistics_registry.h"
#include "main/command_executor.h"
#ifdef PORTFOLIO_BUILD
@@ -50,6 +49,7 @@
#include "smt_util/command.h"
#include "util/configuration.h"
#include "util/result.h"
+#include "util/statistics_registry.h"
using namespace std;
using namespace CVC4;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback