mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

Merge pull request #1076 from chaserhkj/default-pp-mode-api

Browse source 
Fix Z3_PRINT_SMTLIB_FULL not working as expected
This commit is contained in:
Nikolaj Bjorner 2017-06-14 03:04:22 -07:00 • committed by GitHub
commit 2d1abf2795
1 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_ast.cpp
View file

@ -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;