From 60b405aaa9a29acabd65abe16ea6d59afd84983c Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 10 May 2022 11:23:51 +0200 Subject: [PATCH] Support new z3 AST node --- libsmtutil/Z3Interface.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 3a5c75bf3..a0d50d225 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -298,6 +298,7 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr) arguments.push_back(fromZ3Expr(_expr.arg(i))); auto kind = _expr.decl().decl_kind(); + if (_expr.is_ite()) return Expression::ite(arguments[0], arguments[1], arguments[2]); else if (_expr.is_not()) @@ -371,7 +372,10 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr) return Expression("dt_accessor_" + _expr.decl().name().str(), arguments, sort); else if (kind == Z3_OP_DT_IS) return Expression("dt_is", {arguments.at(0)}, sort); - else if (kind == Z3_OP_UNINTERPRETED) + else if ( + kind == Z3_OP_UNINTERPRETED || + kind == Z3_OP_RECURSIVE + ) return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort())); smtAssert(false, "");