Removed assertion, but added another check

mCRL2org · Sep 12, 2024 · fbe52dc · fbe52dc
1 parent ac2ed26
commit fbe52dc
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git 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
@@ -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()))
     {