diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index c80b75ba6..d6b39c394 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3389,6 +3389,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
                 literal lit = *it;                
                 if (value(lit) != l_undef) {
                     ++num_fixed;
+                    if (value(lit) == l_true && lvl(lit) == 1) {
+                        VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
+                    }
                     continue;
                 }
                 push();
diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp
index 3387e1a8e..c34e109d3 100644
--- a/src/test/cnf_backbones.cpp
+++ b/src/test/cnf_backbones.cpp
@@ -271,9 +271,9 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
 
 void tst_cnf_backbones(char ** argv, int argc, int& i) {
     if (i + 1 < argc) {
-        bool use_chunk = (i + 2 < argc && argv[i + 2] == std::string("chunk"));
+        bool use_chunk = (i + 2 < argc && argv[i + 1] == std::string("chunk"));
+        if (use_chunk) ++i;        
         cnf_backbones(use_chunk, argv[i + 1]);
         ++i;
-        if (use_chunk) ++i;
     }
 }