diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index 48fdbd328..630eb0619 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -87,7 +87,7 @@ void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*
 	);
 }
 
-pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
+tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
 {
 	string accumulated{};
 	swap(m_accumulatedOutput, accumulated);
@@ -118,8 +118,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expre
 	else
 		result = CheckResult::ERROR;
 
-	// TODO collect invariants or counterexamples.
-	return {result, {}};
+	return {result, Expression(true), {}};
 }
 
 void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h
index 460895e3b..a7dfb7692 100644
--- a/libsmtutil/CHCSmtLib2Interface.h
+++ b/libsmtutil/CHCSmtLib2Interface.h
@@ -44,7 +44,9 @@ public:
 
 	void addRule(Expression const& _expr, std::string const& _name) override;
 
-	std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
+	/// Takes a function application _expr and checks for reachability.
+	/// @returns solving result, an invariant, and counterexample graph, if possible.
+	std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override;
 
 	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
 
diff --git a/libsmtutil/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h
index 203255345..8385c1c40 100644
--- a/libsmtutil/CHCSolverInterface.h
+++ b/libsmtutil/CHCSolverInterface.h
@@ -54,8 +54,8 @@ public:
 	};
 
 	/// Takes a function application _expr and checks for reachability.
-	/// @returns solving result and a counterexample graph, if possible.
-	virtual std::pair<CheckResult, CexGraph> query(
+	/// @returns solving result, an invariant, and counterexample graph, if possible.
+	virtual std::tuple<CheckResult, Expression, CexGraph> query(
 		Expression const& _expr
 	) = 0;
 
diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp
index 1196b27ff..82dca4878 100644
--- a/libsmtutil/Z3CHCInterface.cpp
+++ b/libsmtutil/Z3CHCInterface.cpp
@@ -77,7 +77,7 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
 	}
 }
 
-pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
+tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
 {
 	CheckResult result;
 	try
@@ -93,15 +93,15 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 			if (m_version >= tuple(4, 8, 8, 0))
 			{
 				auto proof = m_solver.get_answer();
-				return {result, cexGraph(proof)};
+				return {result, Expression(true), cexGraph(proof)};
 			}
 			break;
 		}
 		case z3::check_result::unsat:
 		{
 			result = CheckResult::UNSATISFIABLE;
-			// TODO retrieve invariants.
-			break;
+			auto invariants = m_z3Interface->fromZ3Expr(m_solver.get_answer());
+			return {result, move(invariants), {}};
 		}
 		case z3::check_result::unknown:
 		{
@@ -125,7 +125,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 			result = CheckResult::ERROR;
 	}
 
-	return {result, {}};
+	return {result, Expression(true), {}};
 }
 
 void Z3CHCInterface::setSpacerOptions(bool _preProcessing)
diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h
index a0e4bfa67..5a768f65c 100644
--- a/libsmtutil/Z3CHCInterface.h
+++ b/libsmtutil/Z3CHCInterface.h
@@ -43,7 +43,7 @@ public:
 
 	void addRule(Expression const& _expr, std::string const& _name) override;
 
-	std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
+	std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override;
 
 	Z3Interface* z3Interface() const { return m_z3Interface.get(); }