diff --git a/libraries/pbes/include/mcrl2/pbes/pbesinst_lazy_counter_example.h b/libraries/pbes/include/mcrl2/pbes/pbesinst_lazy_counter_example.h
index d49dbbcfd7..19a1ea97aa 100644
--- a/libraries/pbes/include/mcrl2/pbes/pbesinst_lazy_counter_example.h
+++ b/libraries/pbes/include/mcrl2/pbes/pbesinst_lazy_counter_example.h
@@ -46,8 +46,6 @@ static void rewrite_star(pbes_expression& result,
   if (it != mapping.end())
   {
     structure_graph::index_type index = it->second;
-    assert(G.decoration(index) != structure_graph::d_true && G.decoration(index) != structure_graph::d_false);
-
     std::unordered_set<structure_graph::index_type> todo = {index};
     std::unordered_set<structure_graph::index_type> done;
 
diff --git a/libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h b/libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h
index 9148fee275..4ccc021884 100644
--- a/libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h
+++ b/libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h
@@ -300,6 +300,11 @@ class pbessolve_tool
             << "Warning: the PBES has counter example information, but no witness will be generated due to lack of --file"
             << std::endl;
       }
+
+      if (options.optimization > 0)
+      {
+        throw mcrl2::runtime_error("Counter example PBES can not be solved with --long-strategy greater than 0.");
+      }
     }
     else if ((!lpsfile.empty() || !ltsfile.empty()))
     {