summaryrefslogtreecommitdiff
path: root/src/smt/interpolation_solver.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/interpolation_solver.h')
-rw-r--r--src/smt/interpolation_solver.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
index 8e6d2cd14..096cf8983 100644
--- a/src/smt/interpolation_solver.h
+++ b/src/smt/interpolation_solver.h
@@ -71,8 +71,8 @@ class InterpolationSolver
* the interpolation problem (interpol), and the solution implies the goal
* (conj). If these criteria are not met, an internal error is thrown.
*/
- void checkInterpol(Expr interpol,
- const std::vector<Expr>& easserts,
+ void checkInterpol(Node interpol,
+ const std::vector<Node>& easserts,
const Node& conj);
private:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback