Merge pull request #229 from diffblue/show-formula-loop

ebmc: show-formula now includes lasso constraints

Author: kroening

regression/ebmc/SVA-LTL/lasso1-show-formula.desc

@@ -0,0 +1,8 @@
+CORE
+lasso1.sv
+--bound 1 --show-formula
+^EXIT=0$
+^SIGNAL=0$
+^\(\d+\) lasso::1-back-to-0 ⇔ \(.*counter@1 = .*counter@0 ∧ .*clock@1 ⇔ .*clock@0\)$
+--
+--

src/ebmc/ebmc_base.cpp

@@ -91,6 +91,8 @@ void ebmc_baset::word_level_properties(decision_proceduret &solver)
 {
   const namespacet ns(transition_system.symbol_table);
 
+  message.status() << "Properties" << messaget::eom;
+
   for(propertyt &property : properties.properties)
   {
     if(property.is_disabled())
@@ -104,6 +106,14 @@ void ebmc_baset::word_level_properties(decision_proceduret &solver)
       bound + 1,
       ns);
   }
+
+  // lasso constraints, if needed
+  if(property_requires_lasso_constraints())
+  {
+    message.status() << "Adding lasso constraints" << messaget::eom;
+    lasso_constraints(
+      solver, bound + 1, ns, transition_system.main_symbol->name);
+  }
 }
 
 /*******************************************************************\
@@ -122,14 +132,6 @@ int ebmc_baset::finish_word_level_bmc(stack_decision_proceduret &solver)
 {
   const namespacet ns(transition_system.symbol_table);
 
-  // lasso constraints, if needed
-  if(property_requires_lasso_constraints())
-  {
-    message.status() << "Adding lasso constraints" << messaget::eom;
-    lasso_constraints(
-      solver, bound + 1, ns, transition_system.main_symbol->name);
-  }
-
   message.status() << "Solving with " << solver.decision_procedure_text()
                    << messaget::eom;
 
@@ -367,8 +369,6 @@ int ebmc_baset::do_word_level_bmc(
         ns,
         true);
 
-      message.status() << "Properties" << messaget::eom;
-
       // convert the properties
       word_level_properties(solver);