diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index c6f594d4e..f1080676d 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -101,9 +101,10 @@ public: resize_data(0); #if _WINDOWS errno_t err = fopen_s(&m_file, fname, "rb"); - m_ok = err == 0; + m_ok = (m_file != NULL) && (err == 0); #else m_file = fopen(fname, "rb"); + m_ok = (m_file != NULL); #endif } ~line_reader() { diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index 09db4bde2..deb1300ea 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -62,8 +62,9 @@ void dl_context_saturate_file(params_ref & params, const char * f) { ctx.updt_params(params); datalog::parser * parser = datalog::parser::create(ctx, m); - if (!parser->parse_file(f)) { + if (!parser || !parser->parse_file(f)) { warning_msg("ERROR: failed to parse file"); + dealloc(parser); return; } dealloc(parser); diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index 9e0f285c7..ab5141b18 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -64,7 +64,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, ctx_q.updt_params(params); { parser* p = parser::create(ctx_q,m); - bool ok = p->parse_file(problem_file); + bool ok = p && p->parse_file(problem_file); dealloc(p); if (!ok) { std::cout << "Could not parse: " << problem_file << "\n"; diff --git a/src/test/pdr.cpp b/src/test/pdr.cpp index a1410b482..d95a55a24 100644 --- a/src/test/pdr.cpp +++ b/src/test/pdr.cpp @@ -27,7 +27,7 @@ struct test_model_search { }; ast_manager m; - smt_params smt_params; + smt_params m_smt_params; fixedpoint_params fp_params; context ctx; manager pm; @@ -40,8 +40,8 @@ struct test_model_search { test_model_search(): - ctx(smt_params, fp_params, m), - pm(smt_params, 10, m), + ctx(m_smt_params, fp_params, m), + pm(m_smt_params, 10, m), fn(m), initt(fn), pt(ctx, pm, fn),