mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
fa93bc419d
commit
ef6339f14c
|
@ -2203,9 +2203,8 @@ static void check_error(z3::context& ctx) {
|
|||
static void display_tptp(std::ostream& out) {
|
||||
// run SMT2 parser, pretty print TFA format.
|
||||
z3::context ctx;
|
||||
Z3_ast _fml = Z3_parse_smtlib2_file(ctx, g_input_file, 0, 0, 0, 0, 0, 0);
|
||||
check_error(ctx);
|
||||
z3::expr fml(ctx, _fml);
|
||||
z3::expr_vector fmls = ctx.parse_file(g_input_file);
|
||||
z3::expr fml = z3::mk_and(fmls);
|
||||
|
||||
pp_tptp pp(ctx);
|
||||
pp.collect_decls(fml);
|
||||
|
|
|
@ -1830,8 +1830,9 @@ namespace smt {
|
|||
ast_manager& m = get_manager();
|
||||
smt_params fp;
|
||||
kernel k(m, fp);
|
||||
expr_ref notB(m.mk_not(B), m);
|
||||
k.assert_expr(A);
|
||||
k.assert_expr(m.mk_not(B));
|
||||
k.assert_expr(notB);
|
||||
lbool is_sat = k.check();
|
||||
validating = false;
|
||||
std::cout << is_sat << "\n";
|
||||
|
|
Loading…
Reference in a new issue