summaryrefslogtreecommitdiff
path: root/src/prop/minisat/minisat.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat/minisat.h')
-rw-r--r--src/prop/minisat/minisat.h8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 472ded34e..7dfeb6aa2 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -20,7 +20,7 @@
#include "prop/minisat/simp/SimpSolver.h"
#include "util/statistics_registry.h"
-namespace CVC4 {
+namespace CVC5 {
namespace prop {
class MinisatSatSolver : public CDCLTSatSolverInterface
@@ -40,7 +40,7 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause);
void initialize(context::Context* context,
TheoryProxy* theoryProxy,
- CVC4::context::UserContext* userContext,
+ CVC5::context::UserContext* userContext,
ProofNodeManager* pnm) override;
ClauseId addClause(SatClause& clause, bool removable) override;
@@ -118,5 +118,5 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
}; /* class MinisatSatSolver */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+} // namespace prop
+} // namespace CVC5
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback