From e3f32ca3a8820e4f26615fe366ffc1b96aca9f2a Mon Sep 17 00:00:00 2001
From: "KangJing Huang (Chaserhkj)" <huangkangjing@gmail.com>
Date: Wed, 14 Jun 2017 02:18:21 -0400
Subject: [PATCH] Fix Z3_PRINT_SMTLIB_FULL not working as expected
---
src/api/api_ast.cpp | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 3cec4ec02..7342b3c49 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -821,9 +821,13 @@ extern "C" {
RESET_ERROR_CODE();
std::ostringstream buffer;
switch (mk_c(c)->get_print_mode()) {
- case Z3_PRINT_SMTLIB_FULL:
- buffer << mk_pp(to_ast(a), mk_c(c)->m());
+ case Z3_PRINT_SMTLIB_FULL: {
+ params_ref p;
+ p.set_uint("max_depth", 4294967295u);
+ p.set_uint("min_alias_size", 4294967295u);
+ buffer << mk_pp(to_ast(a), mk_c(c)->m(), p);
break;
+ }
case Z3_PRINT_LOW_LEVEL:
buffer << mk_ll_pp(to_ast(a), mk_c(c)->m());
break;
@@ -1066,7 +1070,7 @@ extern "C" {
case OP_BIT2BOOL: return Z3_OP_BIT2BOOL;
case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
- case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
+ case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSDIV_I: return Z3_OP_BSDIV_I;
case OP_BUDIV_I: return Z3_OP_BUDIV_I;
case OP_BSREM_I: return Z3_OP_BSREM_I;