diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index a5ad7b525..8f92d5bb4 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -181,7 +181,7 @@ extern "C" {
         if (!is) {
             SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
         }
-        else if (ext && std::string("dimacs") == ext) {
+        else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) {
             ast_manager& m = to_solver_ref(s)->get_manager();
             std::stringstream err;
             sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 671184633..182324832 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1197,8 +1197,11 @@ namespace smt {
             literal_vector& lits = get_unhelpful_literals(c, true);
             lits.push_back(c.lit());
             for (unsigned i = 0; i < sz; ++i) {
-                DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
-                add_assign(c, lits, c.lit(i));                               
+                literal lit = c.lit(i);
+                if (ctx.get_assignment(lit) == l_undef) {
+                    DEBUG_CODE(validate_assign(c, lits, lit););
+                    add_assign(c, lits, c.lit(i));               
+                }
             }
         }
     }