From 6de2f866873b68410e093f9c7b0bd6ed760e56a8 Mon Sep 17 00:00:00 2001 From: hwu71 Date: Sat, 24 Jun 2023 00:20:56 -0400 Subject: [PATCH] Temporary fix for z3 op_raw_If --- claripy/backends/backend_z3.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/claripy/backends/backend_z3.py b/claripy/backends/backend_z3.py index 0f4989ac4..c3530f4bc 100644 --- a/claripy/backends/backend_z3.py +++ b/claripy/backends/backend_z3.py @@ -1064,7 +1064,15 @@ def _op_raw_Not(self, a): def _op_raw_If(self, i, t, e): # partially copied from z3._to_expr_ref ctx_ref = self._context.ref() - ast = z3.Z3_mk_ite(ctx_ref, i.as_ast(), t.as_ast(), e.as_ast()) + try: + ast = z3.Z3_mk_ite(ctx_ref, i.as_ast(), t.as_ast(), e.as_ast()) + except Exception as ex: + print("\ni", i) + print("\nt", t) + print("\ne", e) + print("EXCEPTION", ex) + raise ex + k = z3.Z3_get_ast_kind(ctx_ref, ast) sk = z3.Z3_get_sort_kind(ctx_ref, z3.Z3_get_sort(ctx_ref, ast)) if sk == z3.Z3_BOOL_SORT: