summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat/utils/System.cc
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/bvminisat/utils/System.cc')
-rw-r--r--src/prop/bvminisat/utils/System.cc5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/prop/bvminisat/utils/System.cc b/src/prop/bvminisat/utils/System.cc
index aba0a5ac5..9b9f99eb5 100644
--- a/src/prop/bvminisat/utils/System.cc
+++ b/src/prop/bvminisat/utils/System.cc
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <stdio.h>
#include <stdlib.h>
-namespace CVC4 {
+namespace CVC5 {
namespace BVMinisat {
// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
@@ -95,6 +95,5 @@ double BVMinisat::memUsed() {
return 0; }
#endif
-
-} /* CVC4::BVMinisat namespace */
+} /* CVC5::BVMinisat namespace */
} /* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback