diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 772440b42..facbf6c0a 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -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);
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index e34a16eec..4c2d8e8c6 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -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";