diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h
index f9306a936..8286f75db 100644
--- a/src/formula/Ltl/AbstractLtlFormula.h
+++ b/src/formula/Ltl/AbstractLtlFormula.h
@@ -79,7 +79,7 @@ public:
 	 *	@param visitor The visitor object.
 	 *	@return true iff all subtrees are valid.
 	 */
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const = 0;
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const = 0;
 };
 
 } /* namespace ltl */
diff --git a/src/formula/Ltl/And.h b/src/formula/Ltl/And.h
index 2afe2b3fb..c2a43e920 100644
--- a/src/formula/Ltl/And.h
+++ b/src/formula/Ltl/And.h
@@ -53,7 +53,7 @@ class IAndVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitAnd(const And<T>& obj) const = 0;
+		virtual void visitAnd(const And<T>& obj) = 0;
 };
 
 /*!
@@ -135,7 +135,7 @@ public:
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IAndVisitor>()->visitAnd(*this);
 	}
 
diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h
index 1bf5f2f5b..5dd9004cd 100644
--- a/src/formula/Ltl/Ap.h
+++ b/src/formula/Ltl/Ap.h
@@ -51,7 +51,7 @@ class IApVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitAp(const Ap<T>& obj) const = 0;
+		virtual void visitAp(const Ap<T>& obj) = 0;
 };
 
 /*!
@@ -118,7 +118,7 @@ public:
 		return new Ap(this->getAp());
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IApVisitor>()->visitAp(*this);
 	}
 };
diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h
index acb3a77d0..6978bfb45 100644
--- a/src/formula/Ltl/BoundedEventually.h
+++ b/src/formula/Ltl/BoundedEventually.h
@@ -54,7 +54,7 @@ class IBoundedEventuallyVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitBoundedEventually(const BoundedEventually<T>& obj) const = 0;
+		virtual void visitBoundedEventually(const BoundedEventually<T>& obj) = 0;
 };
 
 /*!
@@ -134,7 +134,7 @@ public:
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IBoundedEventuallyVisitor>()->visitBoundedEventually(*this);
 	}
 };
diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h
index be33662a7..334081145 100644
--- a/src/formula/Ltl/BoundedUntil.h
+++ b/src/formula/Ltl/BoundedUntil.h
@@ -53,7 +53,7 @@ class IBoundedUntilVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitBoundedUntil(const BoundedUntil<T>& obj) const = 0;
+		virtual void visitBoundedUntil(const BoundedUntil<T>& obj) = 0;
 };
 
 /*!
@@ -151,7 +151,7 @@ public:
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IBoundedUntilVisitor>()->visitBoundedUntil(*this);
 	}
 };
diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h
index ee6da1243..2fe7bfb97 100644
--- a/src/formula/Ltl/Eventually.h
+++ b/src/formula/Ltl/Eventually.h
@@ -51,7 +51,7 @@ class IEventuallyVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitEventually(const Eventually<T>& obj) const = 0;
+		virtual void visitEventually(const Eventually<T>& obj) = 0;
 };
 
 /*!
@@ -128,7 +128,7 @@ public:
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IEventuallyVisitor>()->visitEventually(*this);
 	}
 };
diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h
index 0dad8c6ac..4d15fe92d 100644
--- a/src/formula/Ltl/Globally.h
+++ b/src/formula/Ltl/Globally.h
@@ -52,7 +52,7 @@ class IGloballyVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitGlobally(const Globally<T>& obj) const = 0;
+		virtual void visitGlobally(const Globally<T>& obj) = 0;
 };
 
 /*!
@@ -130,7 +130,7 @@ public:
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IGloballyVisitor>()->visitGlobally(*this);
 	}
 };
diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h
index fa8f6f644..a17af9dbf 100644
--- a/src/formula/Ltl/Next.h
+++ b/src/formula/Ltl/Next.h
@@ -51,7 +51,7 @@ class INextVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitNext(const Next<T>& obj) const = 0;
+		virtual void visitNext(const Next<T>& obj) = 0;
 };
 
 /*!
@@ -128,7 +128,7 @@ public:
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<INextVisitor>()->visitNext(*this);
 	}
 };
diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h
index 88a553e9c..ea0cb737c 100644
--- a/src/formula/Ltl/Not.h
+++ b/src/formula/Ltl/Not.h
@@ -51,7 +51,7 @@ class INotVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitNot(const Not<T>& obj) const = 0;
+		virtual void visitNot(const Not<T>& obj) = 0;
 };
 
 /*!
@@ -124,7 +124,7 @@ public:
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<INotVisitor>()->visitNot(*this);
 	}
 };
diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h
index 446fd7982..33628b388 100644
--- a/src/formula/Ltl/Or.h
+++ b/src/formula/Ltl/Or.h
@@ -50,7 +50,7 @@ class IOrVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitOr(const Or<T>& obj) const = 0;
+		virtual void visitOr(const Or<T>& obj) = 0;
 };
 
 /*!
@@ -129,7 +129,7 @@ public:
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IOrVisitor>()->visitOr(*this);
 	}
 
diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h
index 3e5720fa1..1f37762a3 100644
--- a/src/formula/Ltl/Until.h
+++ b/src/formula/Ltl/Until.h
@@ -51,7 +51,7 @@ class IUntilVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitUntil(const Until<T>& obj) const = 0;
+		virtual void visitUntil(const Until<T>& obj) = 0;
 };
 
 /*!
@@ -145,7 +145,7 @@ public:
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IUntilVisitor>()->visitUntil(*this);
 	}
 };
diff --git a/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h b/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h
index b77d58973..db0ff8956 100644
--- a/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h
+++ b/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h
@@ -49,9 +49,9 @@ public:
 	 * If the model checker is not of the requested type, type casting will fail and result in an exception.
 	 */
 	template <template <class Type> class Target>
-	const Target<T>* as() const {
+	Target<T>* as() {
 		try {
-			const Target<T>* target = dynamic_cast<const Target<T>*>(this);
+			Target<T>* target = dynamic_cast<Target<T>*>(this);
 			return target;
 		} catch (std::bad_cast& bc) {
 			LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<T>).name() << ".");