Address comments from reviews

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

src/2ls/Makefile

@@ -27,7 +27,7 @@ OBJ+= $(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       $(CPROVER_DIR)/src/util/util$(LIBEXT) \
       $(CPROVER_DIR)/src/goto-instrument/unwind$(OBJEXT) \
       $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
-	  $(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
+      $(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
       ../domains/domains$(LIBEXT) \
       ../ssa/ssa$(LIBEXT) \
       ../solver/solver$(LIBEXT) \

src/2ls/cover_goals_ext.h

@@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "../ssa/local_ssa.h"
 #include "../ssa/unwindable_local_ssa.h"
 #include "../domains/incremental_solver.h"
-#include "types.h"
+#include "traces.h"
 
 /// Try to cover some given set of goals incrementally. This can be seen as a
 /// heuristic variant of SAT-based set-cover. No minimality guarantee.

src/2ls/summary_checker_base.h

@@ -25,7 +25,7 @@ Author: Peter Schrammel
 #include <solver/summary_db.h>
 
 #include "cover_goals_ext.h"
-#include "types.h"
+#include "traces.h"
 
 class graphml_witness_extt;
 

src/2ls/types.h renamed to src/2ls/traces.h

@@ -1,13 +1,13 @@
 /*******************************************************************\
 
-Module: Type declarations
+Module: GOTO traces
 
 Author: František Nečas
 
 \*******************************************************************/
 
 /// \file
-/// Type declarations
+/// GOTO traces
 
 #ifndef CPROVER_2LS_2LS_TYPES_H
 #define CPROVER_2LS_2LS_TYPES_H

src/domains/template_generator_base.cpp

@@ -281,9 +281,10 @@ void template_generator_baset::add_var(
   if(var.type().id()==ID_array && options.get_bool_option("arrays"))
   {
     const array_typet &array_type=to_array_type(var.type());
+    if(!array_type.size().is_constant())
+      return;
     mp_integer size;
-    if(array_type.size().is_constant())
-      to_integer(to_constant_expr(array_type.size()), size);
+    to_integer(to_constant_expr(array_type.size()), size);
     for(mp_integer i=0; i<size; i=i+1)
     {
       var_specs.push_back(var_spect());