From 22c0a593e7ab4fe219ac1a76b685a20d0dee40b4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Jun 2015 17:30:10 -0700
Subject: [PATCH] deal with unit test failure cases, fixes #132 #133

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/fp/datalog_parser.cpp | 3 ++-
 src/test/dl_context.cpp       | 3 ++-
 src/test/dl_query.cpp         | 2 +-
 src/test/pdr.cpp              | 6 +++---
 4 files changed, 8 insertions(+), 6 deletions(-)

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),