From 86687f79a456243c67c5792c8f19f996bb103dd5 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 24 Jan 2018 10:57:22 +0000
Subject: [PATCH 1/9] Fix typos in doxygen

---
 jbmc/src/java_bytecode/java_object_factory.cpp | 2 +-
 jbmc/src/java_bytecode/java_types.cpp          | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 3f5a95f879d..1f8ddf3fe38 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1538,7 +1538,7 @@ exprt object_factory(
   return object;
 }
 
-/// Initializes a primitive-typed or referece-typed object tree rooted at
+/// Initializes a primitive-typed or reference-typed object tree rooted at
 /// `expr`, allocating child objects as necessary and nondet-initializing their
 /// members, or if MAY_ or MUST_UPDATE_IN_PLACE is set, re-initializing
 /// already-allocated objects.
diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
index dc838eadd8d..7970f8a9d1d 100644
--- a/jbmc/src/java_bytecode/java_types.cpp
+++ b/jbmc/src/java_bytecode/java_types.cpp
@@ -256,7 +256,7 @@ std::string erase_type_arguments(const std::string &src)
 /// Returns the full class name, skipping over the generics.
 /// \param src: a type descriptor or signature
 ///   1. Signature:  Lcom/package/OuterClass<TT;>.Inner;
-///   2. Descriptor: Lcom.pacakge.OuterClass$Inner;
+///   2. Descriptor: Lcom.package.OuterClass$Inner;
 /// \return The full name of the class like com.package.OuterClass.Inner (for
 ///   both examples).
 std::string gather_full_class_name(const std::string &src)

From bbe8ccacc0bd04ec89cacc261b1e54c9dfb1d66a Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 25 Jan 2018 20:26:51 +0000
Subject: [PATCH 2/9] Java main method must be public

---
 jbmc/src/java_bytecode/java_entry_point.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 7d250b92ec7..734d4f833eb 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -274,12 +274,14 @@ exprt::operandst java_build_arguments(
     bool named_main=has_suffix(config.main, ".main");
     const typet &string_array_type=
       java_type_from_string("[Ljava.lang.String;");
+    // checks whether the function is static and has a single String[] parameter
     bool has_correct_type=
       to_code_type(function.type).return_type().id()==ID_empty &&
       (!to_code_type(function.type).has_this()) &&
       parameters.size()==1 &&
       parameters[0].type().full_eq(string_array_type);
-    is_main=(named_main && has_correct_type);
+    bool public_access = function.type.get(ID_access) == ID_public;
+    is_main = named_main && has_correct_type && public_access;
   }
 
   // we iterate through all the parameters of the function under test, allocate

From 8f2a82eba58b205cd4e8b62d0fce659e51369ced Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 25 Jan 2018 20:33:51 +0000
Subject: [PATCH 3/9] Generalize allow_null to max_nonnull_tree_depth

allow_null only considered the immediate pointer,
but did not allow forcing sub-objects to be
non-null. This is required for example to
ensure the array elements of the argument to
the main() function to be non-null.
The depth argument starts from 1 now to allow
the immediate pointer to be maybe null when
max_nonnull_tree_depth is 0.
---
 .../src/java_bytecode/convert_java_nondet.cpp |  6 +-
 jbmc/src/java_bytecode/java_entry_point.cpp   | 14 +++--
 .../src/java_bytecode/java_object_factory.cpp | 61 +++++--------------
 jbmc/src/java_bytecode/java_object_factory.h  |  4 --
 .../java_static_initializers.cpp              |  7 ++-
 .../java_bytecode/object_factory_parameters.h | 13 ++++
 .../java_bytecode/simple_method_stubbing.cpp  | 14 +++--
 7 files changed, 55 insertions(+), 64 deletions(-)

diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp
index 735ba4400ba..acc3d9bff51 100644
--- a/jbmc/src/java_bytecode/convert_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp
@@ -36,7 +36,7 @@ static goto_programt::targett insert_nondet_init_code(
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  object_factory_parameterst object_factory_parameters,
   const irep_idt &mode)
 {
   // Return if the instruction isn't an assignment
@@ -76,7 +76,8 @@ static goto_programt::targett insert_nondet_init_code(
   }
 
   // Check whether the nondet object may be null
-  const auto nullable=to_side_effect_expr_nondet(side_effect).get_nullable();
+  if(!to_side_effect_expr_nondet(side_effect).get_nullable())
+    object_factory_parameters.max_nonnull_tree_depth = 1;
   // Get the symbol to nondet-init
   const auto source_loc=target->source_location;
 
@@ -92,7 +93,6 @@ static goto_programt::targett insert_nondet_init_code(
     source_loc,
     true,
     allocation_typet::DYNAMIC,
-    nullable,
     object_factory_parameters,
     update_in_placet::NO_UPDATE_IN_PLACE);
 
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 734d4f833eb..0046aae9405 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -217,6 +217,10 @@ static void java_static_lifetime_init(
           if(allow_null && is_non_null_library_global(nameid))
             allow_null = false;
         }
+        object_factory_parameterst parameters = object_factory_parameters;
+        if(!allow_null)
+          parameters.max_nonnull_tree_depth = 1;
+
         gen_nondet_init(
           sym.symbol_expr(),
           code_block,
@@ -224,8 +228,7 @@ static void java_static_lifetime_init(
           source_location,
           false,
           allocation_typet::GLOBAL,
-          allow_null,
-          object_factory_parameters,
+          parameters,
           pointer_type_selector,
           update_in_placet::NO_UPDATE_IN_PLACE);
       }
@@ -299,10 +302,10 @@ exprt::operandst java_build_arguments(
     // be null
     bool is_this=(param_number==0) && parameters[param_number].get_this();
 
-    bool allow_null=
-      !assume_init_pointers_not_null && !is_main && !is_this;
-
     object_factory_parameterst parameters = object_factory_parameters;
+    if(assume_init_pointers_not_null || is_main || is_this)
+      parameters.max_nonnull_tree_depth = 1;
+
     parameters.function_id = goto_functionst::entry_point();
 
     // generate code to allocate and non-deterministicaly initialize the
@@ -311,7 +314,6 @@ exprt::operandst java_build_arguments(
       p.type(),
       base_name,
       init_code,
-      allow_null,
       symbol_table,
       parameters,
       allocation_typet::LOCAL,
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 1f8ddf3fe38..b44744f8175 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -113,7 +113,6 @@ class java_object_factoryt
     allocation_typet alloc_type,
     bool override_,
     const typet &override_type,
-    bool allow_null,
     size_t depth,
     update_in_placet);
 
@@ -124,7 +123,6 @@ class java_object_factoryt
     const irep_idt &class_identifier,
     allocation_typet alloc_type,
     const pointer_typet &pointer_type,
-    bool allow_null,
     size_t depth,
     const update_in_placet &update_in_place);
 
@@ -434,7 +432,6 @@ void java_object_factoryt::gen_pointer_target_init(
       alloc_type,
       false,   // override
       typet(), // override type immaterial
-      true,    // allow_null always enabled in sub-objects
       depth+1,
       update_in_place);
   }
@@ -717,11 +714,6 @@ static bool add_nondet_string_pointer_initialization(
 ///   others.
 /// \param alloc_type:
 ///   Allocation type (global, local or dynamic)
-/// \param allow_null:
-///   true iff the the non-det initialization code is allowed to set null as a
-///   value to the pointer \p expr; note that the current value of allow_null is
-///   _not_ inherited by subsequent recursive calls; those will always be
-///   authorized to assign null to a pointer
 /// \param depth:
 ///   Number of times that a pointer has been dereferenced from the root of the
 ///   object tree that we are initializing.
@@ -738,7 +730,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
   const irep_idt &class_identifier,
   allocation_typet alloc_type,
   const pointer_typet &pointer_type,
-  bool allow_null,
   size_t depth,
   const update_in_placet &update_in_place)
 {
@@ -843,7 +834,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // Note string-type-specific initialization might fail, e.g. if java.lang.CharSequence does not
   // have the expected fields (typically this happens if --refine-strings was not passed). In this
   // case we fall back to normal pointer target init.
-
   bool string_init_succeeded = false;
 
   if(java_string_library_preprocesst::implements_java_char_sequence_pointer(
@@ -873,6 +863,9 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   auto set_null_inst=get_null_assignment(expr, pointer_type);
 
+  const bool allow_null =
+    depth > object_factory_parameters.max_nonnull_tree_depth;
+
   // Alternatively, if this is a void* we *must* initialise with null:
   // (This can currently happen for some cases of #exception_value)
   bool must_be_null=
@@ -977,7 +970,6 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
     alloc_type,
     false,   // override
     typet(), // override_type
-    true,    // allow_null
     depth,
     update_in_placet::NO_UPDATE_IN_PLACE);
 
@@ -1099,7 +1091,6 @@ void java_object_factoryt::gen_nondet_struct_init(
         alloc_type,
         false,   // override
         typet(), // override_type
-        true,    // allow_null always true for sub-objects
         depth,
         substruct_in_place);
     }
@@ -1149,9 +1140,6 @@ void java_object_factoryt::gen_nondet_struct_init(
 ///   If true, initialize with `override_type` instead of `expr.type()`. Used at
 ///   the moment for reference arrays, which are implemented as void* arrays but
 ///   should be init'd as their true type with appropriate casts.
-/// \param allow_null:
-///   True iff the the non-det initialization code is allowed to set null as a
-///   value to a pointer.
 /// \param depth:
 ///   Number of times that a pointer has been dereferenced from the root of the
 ///   object tree that we are initializing.
@@ -1171,7 +1159,6 @@ void java_object_factoryt::gen_nondet_init(
   allocation_typet alloc_type,
   bool override_,
   const typet &override_type,
-  bool allow_null,
   size_t depth,
   update_in_placet update_in_place)
 {
@@ -1198,7 +1185,6 @@ void java_object_factoryt::gen_nondet_init(
       class_identifier,
       alloc_type,
       pointer_type,
-      allow_null,
       depth,
       update_in_place);
   }
@@ -1278,14 +1264,13 @@ void java_object_factoryt::allocate_nondet_length_array(
   gen_nondet_init(
     assignments,
     length_sym_expr,
-    false,   // is_sub
+    false, // is_sub
     irep_idt(),
-    false,   // skip_classid
+    false,                   // skip_classid
     allocation_typet::LOCAL, // immaterial, type is primitive
-    false,   // override
-    typet(), // override type is immaterial
-    false,   // allow_null
-    0,       // depth is immaterial
+    false,                   // override
+    typet(),                 // override type is immaterial
+    0,                       // depth is immaterial, always non-null
     update_in_placet::NO_UPDATE_IN_PLACE);
 
   // Insert assumptions to bound its length:
@@ -1436,7 +1421,6 @@ void java_object_factoryt::gen_nondet_array_init(
     allocation_typet::DYNAMIC,
     true,  // override
     element_type,
-    true,  // allow_null
     depth,
     child_update_in_place);
 
@@ -1486,7 +1470,6 @@ exprt object_factory(
   const typet &type,
   const irep_idt base_name,
   code_blockt &init_code,
-  bool allow_null,
   symbol_table_baset &symbol_table,
   const object_factory_parameterst &parameters,
   allocation_typet alloc_type,
@@ -1522,14 +1505,13 @@ exprt object_factory(
   state.gen_nondet_init(
     assignments,
     object,
-    false,   // is_sub
-    "",      // class_identifier
-    false,   // skip_classid
+    false, // is_sub
+    "",    // class_identifier
+    false, // skip_classid
     alloc_type,
     false,   // override
     typet(), // override_type is immaterial
-    allow_null,
-    0,       // initial depth
+    1,       // initial depth
     update_in_placet::NO_UPDATE_IN_PLACE);
 
   declare_created_symbols(symbols_created, loc, init_code);
@@ -1560,13 +1542,6 @@ exprt object_factory(
 /// \param alloc_type:
 ///   Allocate new objects as global objects (GLOBAL) or as local variables
 ///   (LOCAL) or using malloc (DYNAMIC).
-/// \param allow_null:
-///   When \p expr is a pointer, the non-det initializing code will
-///   unconditionally set \p expr to a non-null object iff \p allow_null is
-///   true. Note that other references down the object hierarchy *can* be null
-///   when \p allow_null is false (as this parameter is not inherited by
-///   subsequent recursive calls).  Has no effect when \p expr is not
-///   pointer-typed.
 /// \param object_factory_parameters:
 ///   Parameters for the generation of non deterministic objects.
 /// \param pointer_type_selector:
@@ -1587,7 +1562,6 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  bool allow_null,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   update_in_placet update_in_place)
@@ -1604,14 +1578,13 @@ void gen_nondet_init(
   state.gen_nondet_init(
     assignments,
     expr,
-    false,   // is_sub
-    "",      // class_identifier
+    false, // is_sub
+    "",    // class_identifier
     skip_classid,
     alloc_type,
     false,   // override
     typet(), // override_type is immaterial
-    allow_null,
-    0,       // initial depth
+    1,       // initial depth
     update_in_place);
 
   declare_created_symbols(symbols_created, loc, init_code);
@@ -1624,7 +1597,6 @@ exprt object_factory(
   const typet &type,
   const irep_idt base_name,
   code_blockt &init_code,
-  bool allow_null,
   symbol_tablet &symbol_table,
   const object_factory_parameterst &object_factory_parameters,
   allocation_typet alloc_type,
@@ -1635,7 +1607,6 @@ exprt object_factory(
     type,
     base_name,
     init_code,
-    allow_null,
     symbol_table,
     object_factory_parameters,
     alloc_type,
@@ -1651,7 +1622,6 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  bool allow_null,
   const object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place)
 {
@@ -1663,7 +1633,6 @@ void gen_nondet_init(
     loc,
     skip_classid,
     alloc_type,
-    allow_null,
     object_factory_parameters,
     pointer_type_selector,
     update_in_place);
diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h
index 0d8ec5f0995..4c69f282bea 100644
--- a/jbmc/src/java_bytecode/java_object_factory.h
+++ b/jbmc/src/java_bytecode/java_object_factory.h
@@ -90,7 +90,6 @@ exprt object_factory(
   const typet &type,
   const irep_idt base_name,
   code_blockt &init_code,
-  bool allow_null,
   symbol_table_baset &symbol_table,
   const object_factory_parameterst &parameters,
   allocation_typet alloc_type,
@@ -101,7 +100,6 @@ exprt object_factory(
   const typet &type,
   const irep_idt base_name,
   code_blockt &init_code,
-  bool allow_null,
   symbol_tablet &symbol_table,
   const object_factory_parameterst &object_factory_parameters,
   allocation_typet alloc_type,
@@ -121,7 +119,6 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  bool allow_null,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   update_in_placet update_in_place);
@@ -133,7 +130,6 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  bool allow_null,
   const object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place);
 
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index 9cc276f6400..a5dfd289cfa 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -781,6 +781,12 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
   {
     const symbol_exprt new_global_symbol =
       symbol_table.lookup_ref(it->second).symbol_expr();
+
+    parameters.max_nonnull_tree_depth =
+      is_non_null_library_global(it->second)
+        ? object_factory_parameters.max_nonnull_tree_depth + 1
+        : object_factory_parameters.max_nonnull_tree_depth;
+
     gen_nondet_init(
       new_global_symbol,
       static_init_body,
@@ -788,7 +794,6 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
       source_locationt(),
       false,
       allocation_typet::DYNAMIC,
-      !is_non_null_library_global(it->second),
       parameters,
       pointer_type_selector,
       update_in_placet::NO_UPDATE_IN_PLACE);
diff --git a/jbmc/src/java_bytecode/object_factory_parameters.h b/jbmc/src/java_bytecode/object_factory_parameters.h
index 17b838242c2..13eb09bf030 100644
--- a/jbmc/src/java_bytecode/object_factory_parameters.h
+++ b/jbmc/src/java_bytecode/object_factory_parameters.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
 #define MAX_NONDET_STRING_LENGTH std::numeric_limits<std::int32_t>::max()
 #define MAX_NONDET_TREE_DEPTH 5
+#define MAX_NONNULL_TREE_DEPTH 0
 
 struct object_factory_parameterst final
 {
@@ -34,6 +35,18 @@ struct object_factory_parameterst final
   /// such depth becomes >= than this maximum value.
   size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH;
 
+  /// To force a certain depth of non-null objects.
+  /// The default is that objects are 'maybe null' up to the nondet tree depth.
+  /// Examples:
+  /// * max_nondet_tree_depth=0, max_nonnull_tree_depth irrelevant
+  ///   pointer initialized to null
+  /// * max_nondet_tree_depth=n, max_nonnull_tree_depth=0
+  ///   pointer and children up to depth n maybe-null, beyond n null
+  /// * max_nondet_tree_depth=n >=m, max_nonnull_tree_depth=m
+  ///   pointer and children up to depth m initialized to non-null,
+  ///   children up to n maybe-null, beyond n null
+  size_t max_nonnull_tree_depth = MAX_NONNULL_TREE_DEPTH;
+
   /// Force string content to be ASCII printable characters when set to true.
   bool string_printable = false;
 
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index 8bd484ed7e5..16a52370fee 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
@@ -106,6 +106,10 @@ void java_simple_method_stubst::create_method_stub_at(
   if(is_constructor)
     to_init = dereference_exprt(to_init, expected_base);
 
+  object_factory_parameterst parameters = object_factory_parameters;
+  if(assume_non_null)
+    parameters.max_nonnull_tree_depth = 1;
+
   // Generate new instructions.
   code_blockt new_instructions;
   gen_nondet_init(
@@ -115,8 +119,7 @@ void java_simple_method_stubst::create_method_stub_at(
     loc,
     is_constructor,
     allocation_typet::DYNAMIC,
-    !assume_non_null,
-    object_factory_parameters,
+    parameters,
     update_in_place ? update_in_placet::MUST_UPDATE_IN_PLACE
                     : update_in_placet::NO_UPDATE_IN_PLACE);
 
@@ -189,6 +192,10 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
       const exprt &to_return = to_return_symbol.symbol_expr();
       if(to_return_symbol.type.id() != ID_pointer)
       {
+        object_factory_parameterst parameters = object_factory_parameters;
+        if(assume_non_null)
+          parameters.max_nonnull_tree_depth = 1;
+
         gen_nondet_init(
           to_return,
           new_instructions,
@@ -196,8 +203,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
           source_locationt(),
           false,
           allocation_typet::LOCAL, // Irrelevant as type is primitive
-          !assume_non_null,
-          object_factory_parameters,
+          parameters,
           update_in_placet::NO_UPDATE_IN_PLACE);
       }
       else

From 751c040532d65cec5aa18c86f35721a889877770 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Fri, 26 Jan 2018 00:24:48 +0000
Subject: [PATCH 4/9] Simplify check whether String model is present

---
 jbmc/src/java_bytecode/java_object_factory.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index b44744f8175..29935ebedfc 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -683,7 +683,8 @@ static bool add_nondet_string_pointer_initialization(
   const struct_typet &struct_type =
     to_struct_type(ns.follow(to_symbol_type(obj.type())));
 
-  if(!struct_type.has_component("data") || !struct_type.has_component("length"))
+  // if no String model is loaded then we cannot construct a String object
+  if(struct_type.get_bool(ID_incomplete_class))
     return true;
 
   const exprt malloc_site = allocate_dynamic_object_with_decl(
@@ -868,8 +869,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   // Alternatively, if this is a void* we *must* initialise with null:
   // (This can currently happen for some cases of #exception_value)
-  bool must_be_null=
-    subtype==empty_typet();
+  bool must_be_null = subtype == empty_typet();
 
   if(must_be_null)
   {

From 7348c74450a4c25dca4e5de71b0a1ddbc52cd02f Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Fri, 26 Jan 2018 00:26:55 +0000
Subject: [PATCH 5/9] Elements of String array argument to Java main cannot be
 null

---
 jbmc/src/java_bytecode/java_entry_point.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 0046aae9405..54a9178bbf4 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -303,8 +303,12 @@ exprt::operandst java_build_arguments(
     bool is_this=(param_number==0) && parameters[param_number].get_this();
 
     object_factory_parameterst parameters = object_factory_parameters;
-    if(assume_init_pointers_not_null || is_main || is_this)
+    // only pointer must be non-null
+    if(assume_init_pointers_not_null || is_this)
       parameters.max_nonnull_tree_depth = 1;
+    // in main() also the array elements of the argument must be non-null
+    if(is_main)
+      parameters.max_nonnull_tree_depth = 2;
 
     parameters.function_id = goto_functionst::entry_point();
 

From b726dd1884fa21ebea56abe27ce5e33ab0f2a166 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 24 Jan 2018 10:47:33 +0000
Subject: [PATCH 6/9] Add regression tests for initialization of Java main args

---
 .../main-args-elements-non-null1/Main.class   | Bin 0 -> 555 bytes
 .../main-args-elements-non-null1/Main.java    |  11 +++++++++++
 .../main-args-elements-non-null1/test.desc    |   8 ++++++++
 .../main-args-elements-non-null2/Main.class   | Bin 0 -> 529 bytes
 .../main-args-elements-non-null2/Main.java    |   9 +++++++++
 .../main-args-elements-non-null2/test.desc    |   8 ++++++++
 .../Main.class                                | Bin 0 -> 518 bytes
 .../Main.java                                 |   7 +++++++
 .../test.desc                                 |   8 ++++++++
 .../jbmc/main-args-non-null1/Main.class       | Bin 0 -> 518 bytes
 .../jbmc/main-args-non-null1/Main.java        |   7 +++++++
 .../jbmc/main-args-non-null1/test.desc        |   8 ++++++++
 .../Main.class                                | Bin 0 -> 533 bytes
 .../Main.java                                 |   8 ++++++++
 .../test.desc                                 |   8 ++++++++
 .../Main.class                                | Bin 0 -> 533 bytes
 .../Main.java                                 |   9 +++++++++
 .../test.desc                                 |   8 ++++++++
 .../jbmc/no-main-args-maybe-null1/Main.class  | Bin 0 -> 518 bytes
 .../jbmc/no-main-args-maybe-null1/Main.java   |   7 +++++++
 .../jbmc/no-main-args-maybe-null1/test.desc   |   8 ++++++++
 .../jbmc/no-main-args-maybe-null2/Main.class  | Bin 0 -> 518 bytes
 .../jbmc/no-main-args-maybe-null2/Main.java   |   7 +++++++
 .../jbmc/no-main-args-maybe-null2/test.desc   |   8 ++++++++
 .../no-main-int-array-maybe-null1/Main.class  | Bin 0 -> 616 bytes
 .../no-main-int-array-maybe-null1/Main.java   |  16 ++++++++++++++++
 .../no-main-int-array-maybe-null1/test.desc   |  12 ++++++++++++
 .../Main.class                                | Bin 0 -> 545 bytes
 .../no-main-multi-array-maybe-null1/Main.java |  11 +++++++++++
 .../no-main-multi-array-maybe-null1/test.desc |  10 ++++++++++
 .../Main.class                                | Bin 0 -> 545 bytes
 .../no-main-multi-array-maybe-null2/Main.java |  11 +++++++++++
 .../no-main-multi-array-maybe-null2/test.desc |  10 ++++++++++
 .../Main.class                                | Bin 0 -> 521 bytes
 .../Main.java                                 |   9 +++++++++
 .../test.desc                                 |  10 ++++++++++
 .../Main.class                                | Bin 0 -> 521 bytes
 .../Main.java                                 |   9 +++++++++
 .../test.desc                                 |  10 ++++++++++
 .../Main$A.class                              | Bin 0 -> 245 bytes
 .../Main.class                                | Bin 0 -> 641 bytes
 .../Main.java                                 |  18 ++++++++++++++++++
 .../test.desc                                 |  11 +++++++++++
 .../Main$A.class                              | Bin 0 -> 245 bytes
 .../Main.class                                | Bin 0 -> 641 bytes
 .../Main.java                                 |  18 ++++++++++++++++++
 .../test.desc                                 |  11 +++++++++++
 47 files changed, 295 insertions(+)
 create mode 100644 jbmc/regression/jbmc/main-args-elements-non-null1/Main.class
 create mode 100644 jbmc/regression/jbmc/main-args-elements-non-null1/Main.java
 create mode 100644 jbmc/regression/jbmc/main-args-elements-non-null1/test.desc
 create mode 100644 jbmc/regression/jbmc/main-args-elements-non-null2/Main.class
 create mode 100644 jbmc/regression/jbmc/main-args-elements-non-null2/Main.java
 create mode 100644 jbmc/regression/jbmc/main-args-elements-non-null2/test.desc
 create mode 100644 jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class
 create mode 100644 jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java
 create mode 100644 jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc
 create mode 100644 jbmc/regression/jbmc/main-args-non-null1/Main.class
 create mode 100644 jbmc/regression/jbmc/main-args-non-null1/Main.java
 create mode 100644 jbmc/regression/jbmc/main-args-non-null1/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java
 create mode 100644 jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc

diff --git a/jbmc/regression/jbmc/main-args-elements-non-null1/Main.class b/jbmc/regression/jbmc/main-args-elements-non-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..4734b3ec778d31c3f89839276946947490d5ffad
GIT binary patch
literal 555
zcmYk3OG^VW6opUb(XrF1_GPX00fGyyU_rXGh*EXsV^I-QTuj?gqT^IDQ-4g?f@>8l
zDAc9kj}mW&+HsTIoZS1}bCd6%_Yr^^mTg!lBw=FKLeYkff`vI7CCpnWGvrs@AmB0-
zJwMnNf!p$Uhk;!(B<jK!;SPhowtmiFG<qG*Fmoh)e$u~dae1ba>Eg~6K0|Ts>gdLO
zaI2o{cdN}%3ctIp3e(NdZQmZd_v8GjdfOY5?Pjkp+x$={PV$&In+oB;M#{kyk_@Go
zx%X%EK+2w^#;U-=f`dgYF=XP*)7A}dhh#RE8XnC_E;~FBl6NL7G8gvgf`+`r3O$oW
z&&Dz()tw?8Oqrq8q0<uWjCQj!1bbGANYk2#M4AB8n4wsuUPFu2YGq_RV&etc0NIMZ
z^@Y?2^ot>k&#`9w*A!HXpg9;6n*^tSA~&1lBSVS-t(>QGcH*iQH3G6Z^9_jsEaM4=
V{t7LI{W(+s6PmND=Ez08^1u3uW+ngt

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/main-args-elements-non-null1/Main.java b/jbmc/regression/jbmc/main-args-elements-non-null1/Main.java
new file mode 100644
index 00000000000..8a81ebbfed6
--- /dev/null
+++ b/jbmc/regression/jbmc/main-args-elements-non-null1/Main.java
@@ -0,0 +1,11 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    if(args.length>1)
+    {
+      assert(args[0] != null); // must hold
+      assert(args[1] != null); // must hold
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc b/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc
new file mode 100644
index 00000000000..3866f268f76
--- /dev/null
+++ b/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/Main.class b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..396d39badf436149eb0a6ff0780d49b256c3e2b3
GIT binary patch
literal 529
zcmYLFO-lkn7=C7Vb#-08&95>DI+%xq@Rmejb<#Q*L3UbokTG3jckRb`=-Ro0gaSJT
z{ix`j#SaE%-g)Qwdgu4=a{-`+T?0BYVFa+HBWplKMn}#-9t9mmhV;JWy4>-^#CFex
zYjsDw&%ini!Md=8cfz2S4{jN>#-z^~;!R=mtLeDQof`?Jhp{DWhHUx1IkcXv>d3MO
z)wbsddvGj?(Y9yx9$MDp5+ADfMoVR*J()T^ekr6*xJ5dLQo@9Rh=~xw4Ec@b*(&IT
z<4hbfmINK!CU#I_NNkYT-68LJ6n4{UjA%|u+2^iscz>-$;k+q5(2yPM(KqSzZ7h+O
z?o_E@G7Rk|-AZ&aIs=tC*sBC0N_)_6(gcVhPPK$Kp!nTlW$}#M8<ZK674_%`kuRus
zb7<d^ulW2J*^nr$APQuhpc@&>GP(Ay`Eo!q75G4K23>oBroKbj=&W)`egKMjD$}NX
GoAf{VfnZ?(

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java
new file mode 100644
index 00000000000..498f6d43056
--- /dev/null
+++ b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java
@@ -0,0 +1,9 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    if(args.length>0) {
+      assert(args[0] != null); // must not fail 
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc b/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc
new file mode 100644
index 00000000000..3866f268f76
--- /dev/null
+++ b/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..53745bf42482301741efeda8329cb6baa6334180
GIT binary patch
literal 518
zcmYLF%TB^T6g|@x3Z=+X#0MrOE|7(6SeQtR26Y9xz?g`uQYK`uw5Bb73_svnO(fAo
zmnMFc@lL~IGxyG&^Sbl<_wfawfn5VSib=$<uA^i?MN!9wfigCAY%vt}tsvljC_Fbf
z7lGAx_<(`+7~)OgitvO%tsdMmXf1ER88U6*@~g?X&;1(-riZa5T!vEhzCE&@th!^l
z!+JOLg*!Z!#B?{b?1zr^IL9ZNwlh~Yy57XM`K6FL$qwlpN(mDNQYI2eGL%=EXN#a0
zzVG>DED1WcP3)k;kX<3K`y+0L6m~UgIkYFG9PmK+e6ZA_aN&d=XvrS-=$mx<HkK_*
zcj{Cy8HP@iZWXGGYOFQ`dyzn->5NB1+5l_FP%oiJP@-w!70MKu+7D8nQ152Yz9mtK
zhz3<sL!KnE)R9}BjB`uFMx+7c^09Zsr_i-$XzCl3mBzwc@?%iUQyDQISrq;OKayTs

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java
new file mode 100644
index 00000000000..3ecee27827a
--- /dev/null
+++ b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java
@@ -0,0 +1,7 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args != null); // must hold
+  }
+}
diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc b/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc
new file mode 100644
index 00000000000..9e275150f52
--- /dev/null
+++ b/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/main-args-non-null1/Main.class b/jbmc/regression/jbmc/main-args-non-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..53745bf42482301741efeda8329cb6baa6334180
GIT binary patch
literal 518
zcmYLF%TB^T6g|@x3Z=+X#0MrOE|7(6SeQtR26Y9xz?g`uQYK`uw5Bb73_svnO(fAo
zmnMFc@lL~IGxyG&^Sbl<_wfawfn5VSib=$<uA^i?MN!9wfigCAY%vt}tsvljC_Fbf
z7lGAx_<(`+7~)OgitvO%tsdMmXf1ER88U6*@~g?X&;1(-riZa5T!vEhzCE&@th!^l
z!+JOLg*!Z!#B?{b?1zr^IL9ZNwlh~Yy57XM`K6FL$qwlpN(mDNQYI2eGL%=EXN#a0
zzVG>DED1WcP3)k;kX<3K`y+0L6m~UgIkYFG9PmK+e6ZA_aN&d=XvrS-=$mx<HkK_*
zcj{Cy8HP@iZWXGGYOFQ`dyzn->5NB1+5l_FP%oiJP@-w!70MKu+7D8nQ152Yz9mtK
zhz3<sL!KnE)R9}BjB`uFMx+7c^09Zsr_i-$XzCl3mBzwc@?%iUQyDQISrq;OKayTs

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/main-args-non-null1/Main.java b/jbmc/regression/jbmc/main-args-non-null1/Main.java
new file mode 100644
index 00000000000..3ecee27827a
--- /dev/null
+++ b/jbmc/regression/jbmc/main-args-non-null1/Main.java
@@ -0,0 +1,7 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args != null); // must hold
+  }
+}
diff --git a/jbmc/regression/jbmc/main-args-non-null1/test.desc b/jbmc/regression/jbmc/main-args-non-null1/test.desc
new file mode 100644
index 00000000000..3866f268f76
--- /dev/null
+++ b/jbmc/regression/jbmc/main-args-non-null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..6e052a7f6f2d868e4b6498e917abe0ca0f49f0fd
GIT binary patch
literal 533
zcmYL_%}WA77{;I3Rae*b+tf;hpo4ix2yaOg_HofV7(sSgb&xS#V|VS3@zAw%1qlUq
zE9j4k-dX&(%*^}F^ZuS^=J)So4xoyn4h`uL{MgWt(V-%(A*&;YO$}QNsa?}?xb2Fu
z<(vw~><oF2fwdU|HDL+&h(Rsw-7xs-;~r;-HH5`4C!-FxuceqSMy9YBGNrr5z<e|-
zL(}S4TCOdu{-GR<v|O`$-!vZ<`e3a)T#)tFcw%??xsaStlQ{blVL(UNKoB8@+?si^
z40>kUW1EcSfQD@Yc@!ApYvomEz`HJmUAO8(dMBmqaYxv^w_;H^cS0BR$ToK9n>6}1
z7SBm{I;mhX46O!L1=<<y{_+g$MG6t2HQ+TFjYJWnvy@&y@w&zGH}d8A6SA*Rrbv|4
zgCB%Hq2A8m`;rXBV?@b{z+@UA8x3))$h<(%#LB<wA%R5F|Bk>En(rAt^$p6Jv&<sr
O{ZNc!nK<d$r2YZm&tZQ6

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java
new file mode 100644
index 00000000000..14e556fa2a2
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java
@@ -0,0 +1,8 @@
+public class Main
+{
+  static void main(String[] args) // not public!
+  {
+    if(args != null && args.length>0)
+      assert(args[0] != null); // allowed to fail
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc
new file mode 100644
index 00000000000..c23c81e2d8d
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..cd3d63768c1ffcf821b6b1c018f74f99d22de8b5
GIT binary patch
literal 533
zcmYL_J5K^Z6ot?10t?IXMnDA;6APq}#L!8M1|JP*fiV%Q1tw$=7PGtfV<>E`)kG3a
zu%qxt8SiX(G&6VZoco<K^ZWNT2T(;(hlX?rer##T=unZ?kkygHwuT*s)V}FB+;+v-
za?XWgc80viz}gIfny`d>!l0H8?ihUaagQ^^8p7h&lTnA;w^B?OBU4xmnbJdJU_P6b
zp=tFiE!P%S|5y%2TCUlBY?@C?eX!OYF3EapJh8j{Qb<myNt{E8FrXuBAczn{Zo@oV
z1--ECu}#KuK*O$qJPHi)jq;{5;9Zx(Zd&yry^~V*xFc-dTeB#fJE04DWE*?*O&Wb0
zi|3>}RVtVaL#sij0_}`;e|ZM>CWVO58t|HoMxuyOEu~jbyl%0)K)yVGLG~TW6p6BW
zv_SY9>irD9AIVTWMwF}wOr`;{2_jA>GM8my?O*kfKqBe?L|_Wd_X?l-0cFEkWs&oK
MD8{Kwob+r`|KO})e*gdg

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java
new file mode 100644
index 00000000000..97ad6061c78
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java
@@ -0,0 +1,9 @@
+public class Main
+{
+  static void main(String[] args) // not public!
+  {
+    if(args != null && args.length>0) {
+      assert(args[0] == null); // allowed to fail
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc
new file mode 100644
index 00000000000..c23c81e2d8d
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..3131f084ffc2b72d0c513b26eca7ba4a230e73ef
GIT binary patch
literal 518
zcmYLFTT22#6#ix}uC8ldGrJfBJy=1$_z)yfSUqVy7(w>5x`T}AZtSl882>=e6(khY
zW6+O^&MaOSI5Tt3cbobB`}hJ-!?p<ng#>i08Yr4jQ82J(qJ(t=8w~kfI|#TR3eOGB
zMPPS_++koHhFD#=B0OPGD|@#LTElZVL%Jzkel;F-xql<UG#J^!Whhqen*;mFt`2Rt
zUu}oJaQnxSm}-Z1@1bQs&hYViZ#Yvn+uqpk@k=3f5-rj>loA$9BrU{|U??p$&*nid
zeBblQSP~3uTG&FFA+tnYcL%%|QrKmyF{F1=N{0u+=gvZl!i8fR&?7t8p>Hzi+gPR~
z-RY!)$uLwcx|L~XwCnp*uonqLifSxs%FznaR3-EX3N0Z23T1-y!4Hz3Q17PDz9mtK
yh-L)Qkt2x=b;&J9#@U5oEm8)uIsF~62@LHSn)(K1sWCT~d>x8)Ds$u_i~K)40bW%A

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java
new file mode 100644
index 00000000000..aa61bf38859
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java
@@ -0,0 +1,7 @@
+public class Main
+{
+  public void main(String[] args) // not static!
+  {
+    assert(args != null); // allowed to fail
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc
new file mode 100644
index 00000000000..c23c81e2d8d
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..203057c9f9267f630bae323493072ef39a475aa7
GIT binary patch
literal 518
zcmYLFTT22#6#ix}uC8ldGrJfBJy=1$_z)yfSUqVy7(w>5x`T}AZtSl882>=e6(khY
zTMzxH=*;4UfipAbe7Bk3zmG2fHEf$OP)I<>s)3>j6$JxpCQ4X0u)&buwS$2Bq43<`
zTm*J^$Q=gOVTjd*E5Z{7wX%21pfx;)Go+is<yYfTm-{yoOoNdvT!v!hzB#a;?CQ{V
z`_*>n3%7qPiK%vI_a0jI;|w3K_l7fNv+a%j9={Y)C($CELn&dwMAAYW35L>A^K2gU
z!uLI&j3vRqriCq(88S=cb$7sfA%$JG8bf*~rF3{8eC{l?C|o$E0X?#V9r`ANzKvx{
z(w$B!m<&VJqFb4EM!UX01$&V|q^QQCrW~yxO;tjVpwI&HuTUmPAN(Ns3H5FY?OPI+
zh-gL-9XXQ7P?y|tWSm_X)*@vfo73MBo50YXp{Z|BmKt+&$=9J+r!q$_vdI4fJB(gb

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java
new file mode 100644
index 00000000000..0fae3e13177
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java
@@ -0,0 +1,7 @@
+public class Main
+{
+  public void main(String[] args) // not static!
+  {
+    assert(args == null); // allowed to fail
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc
new file mode 100644
index 00000000000..c23c81e2d8d
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..69f688d31f13d4c54c919869c4bfc5d378b4e99a
GIT binary patch
literal 616
zcmYLGOG_J37(F*L$<0hACK+uS-=?_GK$U{-f+*2~;A5c_s;kN5QbyxMW+ugd;oe2J
zu2rbeg6<Uhqr`KknlNx5-#OoR&bjmN<<A3v71V9yQMHi6M~RvZ167G}i3uB%n39+l
z7@haxSVc+D3**fo_S#+55fDcLxn>Xs$(n$%u=q{DZ1p-yptKW&YOjCRR?(p*6FBpN
zP$0W-ysde~gT(VscfIozrkp^&>382|*$2IT<g2fN?zDE<xpd<F^c)o6IIv&~)O2CF
z>xDm-H{PvnMNu!J*&(!b;j44)ng;Y3i5Um8m=h=uN&D>+<tH>fEVa7KD^TsIIEYkd
zpg`A2p8&%iq0Se}^94n@rakdwKxm6xi@Z&97u>Urdx#rN#0b}1T4XMiQ07@vFOlH~
zY~CVsg;L`Qg}*Sq-@|--t2_@YL}wZgzcAh~mYUaacT&or;f6Cm;|qUmmNT{Dr_^Q^
zF16<&iCV;qWE8MUyDd7YkY~YkEBg}e2pdKRIaX4`K*i1dhP;9_uVET@$mmS}72Y%H
ODO7dVb@H(k{_qO<fp9Yb

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java
new file mode 100644
index 00000000000..956afcb9993
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java
@@ -0,0 +1,16 @@
+public class Main
+{
+  public static void main(int[] args)
+  {
+    assert(args == null); // allowed to fail
+    assert(args != null); // allowed to fail
+    if(args != null && args.length > 0) {
+      try {
+        int i = args[0];
+      }
+      catch(Exception e) {
+        assert false; // must hold
+      }
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc
new file mode 100644
index 00000000000..46abab6236b
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc
@@ -0,0 +1,12 @@
+CORE
+Main.class
+--function Main.main --java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
+assertion at file Main\.java line 12 function .* bytecode-index 31: SUCCESS
+\*\* 2 of .* failed
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..5a56689bdfbf9419ea00e5906f8cd082f16166c4
GIT binary patch
literal 545
zcmYL_+e!ja6o&sjqmGVap32NJ3JOdtA-qeX=y0V489{k9>PEKN7&Bw<k}uG81qlUq
zXV61MYY!f7)@iTxt$*#`zt0hX64rHSSPa3BB@HPZDi$>?>quioLxv%_WjYSGUD30g
zQ{kA6E^jfgJBC16Si(JIP;)ys48D_Ii!($k!r~YGhX%K=WivfIn8IRM&eiLcj`?I3
zyQbAH)?8ay?E^U(skvtJzG^;B27={gcY@Yyy}sS#=R$%)RRZlvgaI9413`os(sSnV
zROy**_iWlM2Q;i2SVNW}Ht)P_ba>Mxwe!+Rmkwn}wYVc}-kPyUoZF`dy7CU2^iLZ7
z8;hmoc8XLmDTb^;S(ZE_@6QjxUS%U9WCLE2F2Dk!6wB5tC|-5<4axvJ`7yThqi1a7
z)%`ItWGP9KQ}=%m{(^ctgzsA-6%VPCr#&dp_83K^qd=14GbtsH4#X4w4+I9#d@t~+
V?@;E9sVq6~hhiK_@d<B5@*fNoWn};W

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java
new file mode 100644
index 00000000000..7841b610d1f
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java
@@ -0,0 +1,11 @@
+public class Main
+{
+  public static void main(String[][] args)
+  {
+     assert(args == null ||
+     args.length == 0 ||
+     args[0] == null ||
+     args[0].length == 0 ||
+     args[0][0] != null); // allowed to fail
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc
new file mode 100644
index 00000000000..a631452f5f6
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc
@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..ee7b474bda8ffcf30587c5594d0d04c3ff893436
GIT binary patch
literal 545
zcmYL_%Syvg5QhJgq>W8et+v*BsVFGa;02^RMU<+mR>6v(U8TuEPK}8qsqdmM;93O*
zg}QU$Ly2=jZ8vi}GvEAkettjt0BTq?pre>U3e!4D22>Pv%or$RR>vGeVa1Lj9>yZ@
zqeBtd9gn*V?1~}1D|`{}F{stG3kIzoxSV04A$)$)yY2AsTsG6gtu1_pnQFV;=-T)8
zmS_9dTdg=0{`HQW%(Y_MxoO&WgMqPK#~YxHR?rI_ek>#?(<IQQM3^v;H8F+^LwUqJ
z_*Z%qhCxW1<$#WP6AP#?<VT&Soi2A`QadWuJvx-3<nl;_+#Rw=T->7vy7CIk^iMkd
z8_SpFc8XLmDTb^`S%o|!pR(S;o@FC)WYbBJF2Fb@D3+~fP?GA#3zSE!S>IT-`VUyL
z)a`G~k)@<SPNvyUsF&~1z9dpfkOq0$gLT@Tr-*c{lcdR^lv+XuCZ|$wNIyc?o}j6(
UP)3Y@S#mxF#oU+Tr;-(gKMS8_WB>pF

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java
new file mode 100644
index 00000000000..cf11207135f
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java
@@ -0,0 +1,11 @@
+public class Main
+{
+  public static void main(String[][] args)
+  {
+     assert(args == null ||
+     args.length == 0 ||
+     args[0] == null ||
+     args[0].length == 0 ||
+     args[0][0] == null); // allowed to fail
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc
new file mode 100644
index 00000000000..a631452f5f6
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc
@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..3a9613e9e3c5a2e305086aca33719e150483d3b2
GIT binary patch
literal 521
zcmYLFJx{_=6g{t{EtK+&fC?ri4#*&hVUrjQek`B^#zdS7eKAESrY-&$23Kb_kwg>R
z82nMj`x-u$`|iiN=bZa~|Gs7bYS_`CAsc~$4GlRRGO`--Ittj-u*HzsGd+*HzCCih
zGutz}18y;}4ue{^9os)<kjwkG457xz;tYwV?eMGdu*=;W0j9ywv>gV$eBW$Qb|k>D
zwr}<xTjtXO6R!6L3pTwy8oNDyVT;{}*f{8$&!zz#Q3GK_7z(0M9hlBT^>k_O+;vAT
ziHQXb+Xjj#F(lW>>u#U-d@{IhH3oDWL(bx!?Q(0yMdti54d}2AcIj(0`YM(z2zAP2
z&^3rsG^i@k%ji`qQ?NGyM2w;uH0c7wk)T{aFChipoyr`=%IpRCcSsYYD)QkR(Qn9i
zQ-pp5hZJzcNs5SxLnWCol2nnnNK-5QT0jY;(#j{)3AE5FLh=WsHP6zE*jFGKC&F<$
HkjeZ5O4?lD

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java
new file mode 100644
index 00000000000..f05363fe682
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java
@@ -0,0 +1,9 @@
+public class Main
+{
+  public static void main(Main[] args)
+  {
+    if(args != null && args.length > 0) {
+      assert(args[0] == null); // allowed to fail
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc
new file mode 100644
index 00000000000..49668103f1f
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc
@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 12 function .* bytecode-index 15: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..1f0d7a7f55d626c89ec741f29fb2a85343eebada
GIT binary patch
literal 521
zcmYLF%TB^T6g|@dg;L%Ks9<8^0$E66*h!2A9~;mG#zb5dIx)r4nzr~cEZn+Q6G=3|
zohE*i@lL~IbLT$JJ?Gr{{ri{!Xkbf)f_w~NtSKm{kdaqVR8hjZf(?e;j_!Hf^-ah2
zPE1elTijq^J%&irv`znzL9XszGlW`>!5LC*)8-fBQJ=e40!)LEZrTiL^|sxi>_C7M
zU0)yEcl3ujCfXcWb2hc>jNJi0GsSL9Z0rs7M_q%8xP~ZV3?<R1Te^K$KVFzSbzR3L
zF|nXvQ$raQhV%+~*&p(OPX<@5mPNNQ6b$Z}E;p83WX>PcfDY?no4!V&uVU$vP^U}=
zU4uA9jj9U0jNWi<3icv^NKlLfO}YR{q$n5Ab4WpVtM-j@ZT5uXE2IfBHF^IB@lVJ%
zQ-r<*hZJxmNs5SxBSJD!q^Tltk!F_qjeru!WW(=>OrV6G5t82^t#}q*#C{l(b|f5U
H1DV`EOH*9o

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java
new file mode 100644
index 00000000000..2e8139a9e42
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java
@@ -0,0 +1,9 @@
+public class Main
+{
+  public static void main(Main[] args)
+  {
+    if(args != null && args.length > 0) {
+      assert(args[0] != null); // allowed to fail
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc
new file mode 100644
index 00000000000..49668103f1f
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc
@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 12 function .* bytecode-index 15: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class
new file mode 100644
index 0000000000000000000000000000000000000000..47ea25c867b491c8fdbc8422614627439a472646
GIT binary patch
literal 245
zcmW-by=nqM6ot>-)g5<T<6oU3kU}lAu?ztb0z#sNl77|<VPqX)SH;&#6-eO&_)wBF
zTb#LbzI*SPx!wP+0H)|C2$3p0D0BsKp%#MZ#X5U@6@-J~r=T`Jd>KLe-8!>8?K4ws
zbe5AO>%*zonm6lB{GqKI@AO%xh@cdD4D#%G##Aa@IA@A^uFKMtf{q`Z<l22tR@u&M
zk9^3F;|T#j1qf9`y}B_9iljmJ$m)Cb(J$nuYR5dI3Wi)x=mIp+VNFN_w9rQU53`6T
Ab^rhX

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..a1dc746c06325f63ecd7ac5541a2e019a9f2a9a4
GIT binary patch
literal 641
zcmYL_OHbQC6ot>&j-42XgivS-<(*VuB#;n`Rv^@fwo;`43s9xPYLbj9(_mM&(;vfv
zEo&YEsg>w1mHMMl&zMIxb7$^7bMANVzx!Wz0M_xwMII9c*qC(i+J*V>m~t@fVg|Dg
z<{Zomh=zdoISf_2-IYnA5~id;zPTfVu-4cR7_I4ioCZ;td<YWR>Z%S!hXVFy5C-X%
zfVsHzMZnsQI!d6_3_`WrJ87x-K#N&8p_hQWc$B$rXmN2rmF@34^2ehlzuE3Sy1DyN
zFK(+(f&N?294p82r}R+9h=*a61gbi*+LhtA)y5Ot$2g8+4<3r_sDC+F@K8ftpgfT8
zwT@LgCHupC#2wVK4G4^PR1(Ch^XyF2w8zD8%tOp^rFpK{02hZMP_AkwW=v*?$g{%N
z6r*6w`L_@kyl|5|?JUW;@B(AJYiUF?gYn%Zj8l~SzZm)r^Xo0FKYkx||LzR4zPZ+1
z?xUJXD$Cc%^#>|#Z)ElpYyh~l9l|8}W=Oa|zPIEWXT^e1sgwWZGv|5+1dLSd8#t$M
itaDiA6^w!D6SFqR!SLP-cB^JRU$Kwwrw6hb3;zML&T!NK

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java
new file mode 100644
index 00000000000..44b9b6e14f4
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java
@@ -0,0 +1,18 @@
+public class Main
+{
+  public static class A {
+    int x;
+  }
+  public A a;
+
+  public static void main(Main[] args)
+  {
+    assert(args != null); // allowed to fail
+    if(args != null && args.length > 0) {
+      Main m = args[0];
+      if(m != null) {
+        assert(m.a == null); // allowed to fail
+      }
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc
new file mode 100644
index 00000000000..58989b56c0c
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc
@@ -0,0 +1,11 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
+assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
+\*\* 2 of .* failed
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class
new file mode 100644
index 0000000000000000000000000000000000000000..47ea25c867b491c8fdbc8422614627439a472646
GIT binary patch
literal 245
zcmW-by=nqM6ot>-)g5<T<6oU3kU}lAu?ztb0z#sNl77|<VPqX)SH;&#6-eO&_)wBF
zTb#LbzI*SPx!wP+0H)|C2$3p0D0BsKp%#MZ#X5U@6@-J~r=T`Jd>KLe-8!>8?K4ws
zbe5AO>%*zonm6lB{GqKI@AO%xh@cdD4D#%G##Aa@IA@A^uFKMtf{q`Z<l22tR@u&M
zk9^3F;|T#j1qf9`y}B_9iljmJ$m)Cb(J$nuYR5dI3Wi)x=mIp+VNFN_w9rQU53`6T
Ab^rhX

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..59d39c36a2109e5a344d329bf4db87a0ec803566
GIT binary patch
literal 641
zcmYk2OHbQC6ot>&j-42%34ua@QlKOVj094}q6kzG@sKKoc0pAMSWS{qWe7I19exZ8
zwygV5ky?rFsKk##J!2kWGk50RGv|Ky-roJb2C#xT7kP{qU}M6;D;MVdW75HE7gLya
zFyr8jfM^JKAHq<@n_ZbCDq%_r<eR%P2y2ZsfuWkt$7v9S$ySiaR#$Z>IuNkegD^<n
z3z+i@Uj(epsG|f*%^*}CdnYXwf7W6aPUt1z&L3v3Yg$~~OJ)0bSDrp-^6TyHgPXe-
z_2RbL3H0BB=2$wCXVOC%gC1U>Bv93f<*p3BE;k<Gw&OU8J$NXxqyFV!)<X?-fpTB|
zsdc2<DcSGmBW}NzZ9rh8qmm$2ohN6aradl(V;*3JE6sDo2DmsBfpS$dF=H}AM4lDC
zCK&}|&cA~A#tS#e)6SBd3&VKHyOu^YGZ<ID!#GFD|A&D;F!!%u{q=89_pdK7?VE3#
zi#ModlFH&w<esUty^-0EvjO1Jb^sIPn<C*X`QDLhgcS=$rB43QC(e}&2pFu`zu=t1
iu`XemKVbAtADOj54u-cO*sYrN9Ah8dPY+}>7XAaYWN_60

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java
new file mode 100644
index 00000000000..fd829647796
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java
@@ -0,0 +1,18 @@
+public class Main
+{
+  public static class A {
+    int x;
+  }
+  public A a;
+
+  public static void main(Main[] args)
+  {
+    assert(args != null); // allowed to fail
+    if(args != null && args.length > 0) {
+      Main m = args[0];
+      if(m != null) {
+        assert(m.a != null); // allowed to fail
+      }
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc
new file mode 100644
index 00000000000..58989b56c0c
--- /dev/null
+++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc
@@ -0,0 +1,11 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
+assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
+\*\* 2 of .* failed
+--
+^warning: ignoring

From b0470910115f6e3e8362eb17c4b1f62d1ec42c90 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 11 Apr 2018 15:39:50 +0100
Subject: [PATCH 7/9] Simplify main method detection for Java

---
 jbmc/src/java_bytecode/java_entry_point.cpp | 78 ++++++++++-----------
 1 file changed, 36 insertions(+), 42 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 54a9178bbf4..a6fc3018f7e 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_string_literals.h"
 #include "java_utils.h"
 
+#define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
+
 static void create_initialize(symbol_table_baset &symbol_table)
 {
   // If __CPROVER_initialize already exists, replace it. It may already exist
@@ -242,6 +244,27 @@ static void java_static_lifetime_init(
   }
 }
 
+/// Checks whether the given symbol is a valid java main method
+/// i.e. it must be public, static, called 'main' and
+/// have signature void(String[])
+/// \param function: the function symbol
+/// \return true if it is a valid main method
+bool is_java_main(const symbolt &function)
+{
+  bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);
+  const code_typet &function_type = to_code_type(function.type);
+  const typet &string_array_type = java_type_from_string("[Ljava/lang/String;");
+  // checks whether the function is static and has a single String[] parameter
+  bool is_static = !function_type.has_this();
+  // this should be implied by the signature
+  const code_typet::parameterst &parameters = function_type.parameters();
+  bool has_correct_type = function_type.return_type().id() == ID_empty &&
+                          parameters.size() == 1 &&
+                          parameters[0].type().full_eq(string_array_type);
+  bool public_access = function_type.get(ID_access) == ID_public;
+  return named_main && is_static && has_correct_type && public_access;
+}
+
 ///  Extends \p init_code with code that allocates the objects used as test
 ///  arguments for the function under test (\p function) and
 ///  non-deterministically initializes them.
@@ -268,24 +291,7 @@ exprt::operandst java_build_arguments(
   // certain method arguments cannot be allowed to be null, we set the following
   // variable to true iff the method under test is the "main" method, which will
   // be called (by the jvm) with arguments that are never null
-  bool is_default_entry_point(config.main.empty());
-  bool is_main=is_default_entry_point;
-
-  // if walks like a duck and quacks like a duck, it is a duck!
-  if(!is_main)
-  {
-    bool named_main=has_suffix(config.main, ".main");
-    const typet &string_array_type=
-      java_type_from_string("[Ljava.lang.String;");
-    // checks whether the function is static and has a single String[] parameter
-    bool has_correct_type=
-      to_code_type(function.type).return_type().id()==ID_empty &&
-      (!to_code_type(function.type).has_this()) &&
-      parameters.size()==1 &&
-      parameters[0].type().full_eq(string_array_type);
-    bool public_access = function.type.get(ID_access) == ID_public;
-    is_main = named_main && has_correct_type && public_access;
-  }
+  bool is_main = is_java_main(function);
 
   // we iterate through all the parameters of the function under test, allocate
   // an object for that parameter (recursively allocating other objects
@@ -455,37 +461,25 @@ main_function_resultt get_main_symbol(
 
     // are we given a main class?
     if(main_class.empty())
-      return main_function_resultt::NotFound; // silently ignore
-
-    std::string entry_method = id2string(main_class) + ".main";
-
-    std::string prefix="java::"+entry_method+":";
-
-    // look it up
-    std::set<const symbolt *> matches;
-
-    for(const auto &named_symbol : symbol_table.symbols)
     {
-      if(named_symbol.second.type.id() == ID_code
-        && has_prefix(id2string(named_symbol.first), prefix))
-      {
-        matches.insert(&named_symbol.second);
-      }
+      // no, but we allow this situation to output symbol table,
+      // goto functions, etc
+      return main_function_resultt::NotFound;
     }
 
-    if(matches.empty())
-      // Not found, silently ignore
-      return main_function_resultt::NotFound;
+    std::string entry_method =
+      "java::" + id2string(main_class) + "." + JAVA_MAIN_METHOD;
+    const symbolt *symbol = symbol_table.lookup(entry_method);
 
-    if(matches.size() > 1)
+    // has the class a correct main method?
+    if(!symbol || !is_java_main(*symbol))
     {
-      message.error()
-        << "main method in `" << main_class
-        << "' is ambiguous" << messaget::eom;
-      return main_function_resultt::Error;  // give up with error, no main
+      // no, but we allow this situation to output symbol table,
+      // goto functions, etc
+      return main_function_resultt::NotFound;
     }
 
-    return **matches.begin(); // Return found function
+    return *symbol;
   }
 }
 

From 9b1901564fb7943ad0d6823b32419b2213ef25f8 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 10 Jun 2018 15:10:16 +0100
Subject: [PATCH 8/9] Fix tests with incorrect main methods

---
 .../jbmc-strings/bug-test-gen-119-2/test.desc   |   2 +-
 .../jbmc-strings/bug-test-gen-119/test.desc     |   2 +-
 .../regression/jbmc-strings/java_case/test.desc |   2 +-
 .../jbmc-strings/java_case/test_case.java       |   2 +-
 .../jbmc-strings/java_char_array/test.desc      |   2 +-
 .../java_char_array/test_char_array.java        |   2 +-
 .../jbmc-strings/java_char_at/test.desc         |   2 +-
 .../jbmc-strings/java_char_at/test_char_at.java |   2 +-
 .../jbmc-strings/java_code_point/test.desc      |   2 +-
 .../java_code_point/test_code_point.java        |   2 +-
 .../jbmc-strings/java_compare/test.desc         |   2 +-
 .../jbmc-strings/java_compare/test_compare.java |   2 +-
 .../jbmc-strings/java_concat/test.desc          |   2 +-
 .../jbmc-strings/java_concat/test_concat.java   |   2 +-
 .../jbmc-strings/java_contains/test.desc        |   2 +-
 .../java_contains/test_contains.java            |   2 +-
 .../jbmc-strings/java_delete/test.desc          |   2 +-
 .../jbmc-strings/java_delete/test_delete.java   |   2 +-
 .../jbmc-strings/java_delete_char_at/test.desc  |   2 +-
 .../test_delete_char_at.java                    |   2 +-
 .../jbmc-strings/java_empty/test.desc           |   2 +-
 .../jbmc-strings/java_empty/test_empty.java     |   2 +-
 .../jbmc-strings/java_endswith/test.desc        |   2 +-
 .../java_endswith/test_endswith.java            |   2 +-
 .../jbmc-strings/java_hash_code/test.desc       |   2 +-
 .../java_hash_code/test_hash_code.java          |   2 +-
 .../jbmc-strings/java_index_of/test.desc        |   2 +-
 .../java_index_of/test_index_of.java            |   2 +-
 .../jbmc-strings/java_index_of_char/test.desc   |   2 +-
 .../java_index_of_char/test_index_of_char.java  |   2 +-
 .../jbmc-strings/java_insert_char/test.desc     |   2 +-
 .../java_insert_char/test_insert_char.java      |   2 +-
 .../jbmc-strings/java_insert_int/test.desc      |   2 +-
 .../java_insert_int/test_insert_int.java        |   2 +-
 .../jbmc-strings/java_insert_multiple/test.desc |   2 +-
 .../test_insert_multiple.java                   |   2 +-
 .../jbmc-strings/java_insert_string/test.desc   |   2 +-
 .../java_insert_string/test_insert_string.java  |   2 +-
 .../jbmc/NondetCharSequence/test.desc           |   2 +-
 jbmc/regression/jbmc/NondetString/test.desc     |   2 +-
 .../jbmc/NondetStringBuffer/test.desc           |   2 +-
 .../jbmc/NondetStringBuilder/test.desc          |   2 +-
 .../annotations1/show_annotation_symbol.desc    |   2 +-
 jbmc/regression/jbmc/class-fields/test.desc     |   2 +-
 jbmc/regression/jbmc/class-literals/test.desc   |   2 +-
 .../jbmc/class-literals/test_lazy.desc          |   2 +-
 .../regression/jbmc/classtest1/classtest1.class | Bin 351 -> 351 bytes
 jbmc/regression/jbmc/classtest1/classtest1.java |   2 +-
 jbmc/regression/jbmc/exceptions23/test.desc     |   2 +-
 jbmc/regression/jbmc/exceptions24/test.desc     |   2 +-
 jbmc/regression/jbmc/finally1/test.desc         |   2 +-
 jbmc/regression/jbmc/finally2/test.desc         |   2 +-
 jbmc/regression/jbmc/finally3/test.desc         |   2 +-
 jbmc/regression/jbmc/finally4/test.desc         |   2 +-
 jbmc/regression/jbmc/finally5/test.desc         |   2 +-
 jbmc/regression/jbmc/finally6/test.desc         |   2 +-
 jbmc/regression/jbmc/finally7/test.desc         |   2 +-
 jbmc/regression/jbmc/jsr2/test.desc             |   2 +-
 .../method_parameters.class                     | Bin
 .../method_parameters.java                      |   0
 .../test.desc                                   |   0
 .../method_parameters.class                     | Bin
 .../method_parameters.java                      |   0
 .../test.desc                                   |   0
 .../test.desc                                   |   2 +-
 .../test.desc                                   |   2 +-
 .../strings-smoke-tests/java_char_at/test.desc  |   2 +-
 .../java_char_at/test_char_at.java              |   2 +-
 .../java_code_point/test.desc                   |   2 +-
 .../java_code_point/test_code_point.java        |   2 +-
 .../strings-smoke-tests/java_contains/test.desc |   2 +-
 .../java_contains/test_string_printable.desc    |   2 +-
 .../java_delete_char_at/test.desc               |   2 +-
 .../test_delete_char_at.java                    |   2 +-
 .../strings-smoke-tests/java_endswith/test.desc |   2 +-
 .../java_endswith/test_endswith.java            |   2 +-
 .../strings-smoke-tests/java_float/test.desc    |   2 +-
 .../java_float/test_float.java                  |   2 +-
 .../strings-smoke-tests/java_format/test.desc   |   2 +-
 .../strings-smoke-tests/java_format2/test.desc  |   2 +-
 .../strings-smoke-tests/java_format3/test.desc  |   2 +-
 .../java_hash_code/test.desc                    |   2 +-
 .../java_hash_code/test_hash_code.java          |   2 +-
 .../strings-smoke-tests/java_if/test.desc       |   2 +-
 .../strings-smoke-tests/java_index_of/test.desc |   2 +-
 .../java_index_of/test_index_of.java            |   2 +-
 .../java_index_of2/test.desc                    |   2 +-
 .../java_index_of_char/test.desc                |   4 +---
 .../java_index_of_char/test_index_of_char.java  |   2 +-
 .../java_insert_char/test.desc                  |   2 +-
 .../java_insert_char/test_insert_char.java      |   2 +-
 .../java_insert_multiple/test.desc              |   2 +-
 .../test_insert_multiple.java                   |   2 +-
 .../java_insert_string/test.desc                |   2 +-
 .../java_insert_string/test_insert_string.java  |   2 +-
 .../strings-smoke-tests/java_intern/test.desc   |   2 +-
 .../java_intern/test_intern.java                |   2 +-
 .../java_last_index_of/test.desc                |   2 +-
 .../java_last_index_of/test_last_index_of.java  |   2 +-
 .../java_last_index_of_char/test.desc           |   2 +-
 .../test_last_index_of_char.java                |   2 +-
 .../strings-smoke-tests/java_length/test.desc   |   2 +-
 .../java_length/test_length.java                |   2 +-
 .../java_parseint/test3.desc                    |   2 +-
 .../java_replace_char/test.desc                 |   2 +-
 .../java_replace_char/test_replace_char.java    |   2 +-
 .../java_set_char_at/test.desc                  |   2 +-
 .../java_set_char_at/test_set_char_at.java      |   2 +-
 .../java_set_length/test.desc                   |   2 +-
 .../java_set_length/test_set_length.java        |   2 +-
 .../java_starts_with/test.desc                  |   2 +-
 .../java_starts_with/test_starts_with.java      |   2 +-
 .../java_string_builder_length/test.desc        |   2 +-
 .../test_sb_length.java                         |   2 +-
 .../java_subsequence/test.desc                  |   2 +-
 .../java_subsequence/test_subsequence.java      |   2 +-
 .../java_substring/test.desc                    |   2 +-
 .../java_substring/test_substring.java          |   2 +-
 .../strings-smoke-tests/java_trim/test.desc     |   2 +-
 .../java_trim/test_trim.java                    |   2 +-
 .../max_input_length/Test.class                 | Bin 651 -> 655 bytes
 .../max_input_length/Test.java                  |   2 +-
 .../max_input_length/test1.desc                 |   2 +-
 .../max_input_length/test2.desc                 |   2 +-
 124 files changed, 116 insertions(+), 118 deletions(-)
 rename jbmc/regression/jbmc/{method_parmeters1 => method_parameters1}/method_parameters.class (100%)
 rename jbmc/regression/jbmc/{method_parmeters1 => method_parameters1}/method_parameters.java (100%)
 rename jbmc/regression/jbmc/{method_parmeters1 => method_parameters1}/test.desc (100%)
 rename jbmc/regression/jbmc/{method_parmeters2 => method_parameters2}/method_parameters.class (100%)
 rename jbmc/regression/jbmc/{method_parmeters2 => method_parameters2}/method_parameters.java (100%)
 rename jbmc/regression/jbmc/{method_parmeters2 => method_parameters2}/test.desc (100%)

diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc
index 447be05df73..0f52c235798 100644
--- a/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc
+++ b/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOfLong.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function StringValueOfLong.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc
index 22bd78b3cac..c0f9b9e2d82 100644
--- a/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc
+++ b/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOfBool.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function StringValueOfBool.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/java_case/test.desc b/jbmc/regression/jbmc-strings/java_case/test.desc
index 22d58ddb3ac..b194d77cd40 100644
--- a/jbmc/regression/jbmc-strings/java_case/test.desc
+++ b/jbmc/regression/jbmc-strings/java_case/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_case.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_case/test_case.java b/jbmc/regression/jbmc-strings/java_case/test_case.java
index 309abfc07b9..ec66e5ed395 100644
--- a/jbmc/regression/jbmc-strings/java_case/test_case.java
+++ b/jbmc/regression/jbmc-strings/java_case/test_case.java
@@ -1,6 +1,6 @@
 public class test_case
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Ab");
       String l = s.toLowerCase();
diff --git a/jbmc/regression/jbmc-strings/java_char_array/test.desc b/jbmc/regression/jbmc-strings/java_char_array/test.desc
index aaf2c9f8fd4..4cfdbf58a28 100644
--- a/jbmc/regression/jbmc-strings/java_char_array/test.desc
+++ b/jbmc/regression/jbmc-strings/java_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_char_array.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 9.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java b/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java
index 96e250fb030..5028f5afa4d 100644
--- a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java
+++ b/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java
@@ -1,6 +1,6 @@
 public class test_char_array
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = "abc";
       char [] str = s.toCharArray();
diff --git a/jbmc/regression/jbmc-strings/java_char_at/test.desc b/jbmc/regression/jbmc-strings/java_char_at/test.desc
index dd2c1c343ae..8507d50a8fb 100644
--- a/jbmc/regression/jbmc-strings/java_char_at/test.desc
+++ b/jbmc/regression/jbmc-strings/java_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_char_at.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_char_at.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 5.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_char_at/test_char_at.java b/jbmc/regression/jbmc-strings/java_char_at/test_char_at.java
index 9ae02733fb8..17e73b6baf6 100644
--- a/jbmc/regression/jbmc-strings/java_char_at/test_char_at.java
+++ b/jbmc/regression/jbmc-strings/java_char_at/test_char_at.java
@@ -1,6 +1,6 @@
 public class test_char_at {
 
-  public static void main(/*String[] argv*/) {
+  public static void main() {
     String s = new String("abc");
     assert(s.charAt(2)!='c');
   }
diff --git a/jbmc/regression/jbmc-strings/java_code_point/test.desc b/jbmc/regression/jbmc-strings/java_code_point/test.desc
index 322ead7c0a1..cda7f110aba 100644
--- a/jbmc/regression/jbmc-strings/java_code_point/test.desc
+++ b/jbmc/regression/jbmc-strings/java_code_point/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_code_point.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_code_point.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java b/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java
index 345dc1fa08b..266a05c1646 100644
--- a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java
+++ b/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java
@@ -1,6 +1,6 @@
 public class test_code_point
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = "!𐤇𐤄𐤋𐤋𐤅";
       StringBuilder sb = new StringBuilder();
diff --git a/jbmc/regression/jbmc-strings/java_compare/test.desc b/jbmc/regression/jbmc-strings/java_compare/test.desc
index 6b8c890288d..0d7310590bc 100644
--- a/jbmc/regression/jbmc-strings/java_compare/test.desc
+++ b/jbmc/regression/jbmc-strings/java_compare/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_compare.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_compare.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 7.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_compare/test_compare.java b/jbmc/regression/jbmc-strings/java_compare/test_compare.java
index 0a535fd0bf3..1c3c1de86d8 100644
--- a/jbmc/regression/jbmc-strings/java_compare/test_compare.java
+++ b/jbmc/regression/jbmc-strings/java_compare/test_compare.java
@@ -1,6 +1,6 @@
 public class test_compare
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s1 = "ab";
       String s2 = "aa";
diff --git a/jbmc/regression/jbmc-strings/java_concat/test.desc b/jbmc/regression/jbmc-strings/java_concat/test.desc
index 6063f361aa5..b1d47ce246d 100644
--- a/jbmc/regression/jbmc-strings/java_concat/test.desc
+++ b/jbmc/regression/jbmc-strings/java_concat/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_concat.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_concat.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 10.* SUCCESS$
diff --git a/jbmc/regression/jbmc-strings/java_concat/test_concat.java b/jbmc/regression/jbmc-strings/java_concat/test_concat.java
index 9f4d3f5e371..b4b9a54f242 100644
--- a/jbmc/regression/jbmc-strings/java_concat/test_concat.java
+++ b/jbmc/regression/jbmc-strings/java_concat/test_concat.java
@@ -1,6 +1,6 @@
 public class test_concat
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("pi");
       int i = s.length();
diff --git a/jbmc/regression/jbmc-strings/java_contains/test.desc b/jbmc/regression/jbmc-strings/java_contains/test.desc
index c5166216bb1..cfa99b27ba0 100644
--- a/jbmc/regression/jbmc-strings/java_contains/test.desc
+++ b/jbmc/regression/jbmc-strings/java_contains/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_contains.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_contains.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 7.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_contains/test_contains.java b/jbmc/regression/jbmc-strings/java_contains/test_contains.java
index 6f4c60a1a2e..7c0d5304cd3 100644
--- a/jbmc/regression/jbmc-strings/java_contains/test_contains.java
+++ b/jbmc/regression/jbmc-strings/java_contains/test_contains.java
@@ -1,6 +1,6 @@
 public class test_contains
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Abc");
       String u = "bc";
diff --git a/jbmc/regression/jbmc-strings/java_delete/test.desc b/jbmc/regression/jbmc-strings/java_delete/test.desc
index 721165e152d..44af4af9c68 100644
--- a/jbmc/regression/jbmc-strings/java_delete/test.desc
+++ b/jbmc/regression/jbmc-strings/java_delete/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_delete.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_delete/test_delete.java b/jbmc/regression/jbmc-strings/java_delete/test_delete.java
index 62ea5dbf9ce..86ffbb8593a 100644
--- a/jbmc/regression/jbmc-strings/java_delete/test_delete.java
+++ b/jbmc/regression/jbmc-strings/java_delete/test_delete.java
@@ -1,6 +1,6 @@
 public class test_delete
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder s = new StringBuilder("Abc");
       org.cprover.CProverString.delete(s,1,2);
diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc b/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc
index 2ec7b55da93..a61ab36b4b1 100644
--- a/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc
+++ b/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete_char_at.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_delete_char_at.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 9.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java b/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java
index d43a2845f95..ffb4f48a59c 100644
--- a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java
+++ b/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java
@@ -1,6 +1,6 @@
 public class test_delete_char_at
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder s = new StringBuilder();
       s.append("Abc");
diff --git a/jbmc/regression/jbmc-strings/java_empty/test.desc b/jbmc/regression/jbmc-strings/java_empty/test.desc
index 4c9cf9d82eb..32e54658d79 100644
--- a/jbmc/regression/jbmc-strings/java_empty/test.desc
+++ b/jbmc/regression/jbmc-strings/java_empty/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_empty.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_empty.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 6.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_empty/test_empty.java b/jbmc/regression/jbmc-strings/java_empty/test_empty.java
index 18fde4a115e..734d9290ede 100644
--- a/jbmc/regression/jbmc-strings/java_empty/test_empty.java
+++ b/jbmc/regression/jbmc-strings/java_empty/test_empty.java
@@ -1,6 +1,6 @@
 public class test_empty
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String empty = "";
       assert(!empty.isEmpty());
diff --git a/jbmc/regression/jbmc-strings/java_endswith/test.desc b/jbmc/regression/jbmc-strings/java_endswith/test.desc
index 10f8a8b0e2f..9aba187f286 100644
--- a/jbmc/regression/jbmc-strings/java_endswith/test.desc
+++ b/jbmc/regression/jbmc-strings/java_endswith/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_endswith.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_endswith.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 7.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java b/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java
index fabf6f8dde0..5e743a9c569 100644
--- a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java
+++ b/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java
@@ -1,6 +1,6 @@
 public class test_endswith
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Abcd");
       String suff = "cd";
diff --git a/jbmc/regression/jbmc-strings/java_hash_code/test.desc b/jbmc/regression/jbmc-strings/java_hash_code/test.desc
index 70dfc7e6bbe..f863a67e57d 100644
--- a/jbmc/regression/jbmc-strings/java_hash_code/test.desc
+++ b/jbmc/regression/jbmc-strings/java_hash_code/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_hash_code.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_hash_code.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 7.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java b/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java
index fbc15f0b4c2..fb01e0cb67e 100644
--- a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java
+++ b/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java
@@ -1,6 +1,6 @@
 public class test_hash_code
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s1 = "ab";
       String s2 = "ab";
diff --git a/jbmc/regression/jbmc-strings/java_index_of/test.desc b/jbmc/regression/jbmc-strings/java_index_of/test.desc
index b4289558902..4cd2ce43a12 100644
--- a/jbmc/regression/jbmc-strings/java_index_of/test.desc
+++ b/jbmc/regression/jbmc-strings/java_index_of/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_index_of.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java b/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java
index b607ba79570..96763d04847 100644
--- a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java
+++ b/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java
@@ -1,6 +1,6 @@
 public class test_index_of
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = "Abc";
       String bc = "bc";
diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test.desc b/jbmc/regression/jbmc-strings/java_index_of_char/test.desc
index e40554cc835..e91db762b07 100644
--- a/jbmc/regression/jbmc-strings/java_index_of_char/test.desc
+++ b/jbmc/regression/jbmc-strings/java_index_of_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of_char.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_index_of_char.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java b/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java
index 92d75b3b07d..999b50f6896 100644
--- a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java
+++ b/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java
@@ -1,6 +1,6 @@
 public class test_index_of_char
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = "Abc";
       char c = 'c';
diff --git a/jbmc/regression/jbmc-strings/java_insert_char/test.desc b/jbmc/regression/jbmc-strings/java_insert_char/test.desc
index cdda3eeae95..7cd1cde2df7 100644
--- a/jbmc/regression/jbmc-strings/java_insert_char/test.desc
+++ b/jbmc/regression/jbmc-strings/java_insert_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_insert_char.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java b/jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java
index 12dcc8cdb90..12798d84aef 100644
--- a/jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java
+++ b/jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java
@@ -1,6 +1,6 @@
 public class test_insert_char
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder sb = new StringBuilder("ac");
       org.cprover.CProverString.insert(sb, 1, 'b');
diff --git a/jbmc/regression/jbmc-strings/java_insert_int/test.desc b/jbmc/regression/jbmc-strings/java_insert_int/test.desc
index bc25e9abf3c..3fa476250c1 100644
--- a/jbmc/regression/jbmc-strings/java_insert_int/test.desc
+++ b/jbmc/regression/jbmc-strings/java_insert_int/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_int.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_insert_int.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_insert_int/test_insert_int.java b/jbmc/regression/jbmc-strings/java_insert_int/test_insert_int.java
index 2765859866f..9705a0f37b0 100644
--- a/jbmc/regression/jbmc-strings/java_insert_int/test_insert_int.java
+++ b/jbmc/regression/jbmc-strings/java_insert_int/test_insert_int.java
@@ -1,6 +1,6 @@
 public class test_insert_int
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder sb = new StringBuilder("ac");
       org.cprover.CProverString.insert(sb, 1, 42);
diff --git a/jbmc/regression/jbmc-strings/java_insert_multiple/test.desc b/jbmc/regression/jbmc-strings/java_insert_multiple/test.desc
index cae43d53985..c1a8a213da4 100644
--- a/jbmc/regression/jbmc-strings/java_insert_multiple/test.desc
+++ b/jbmc/regression/jbmc-strings/java_insert_multiple/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_multiple.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_insert_multiple.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 9.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java b/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java
index 60daceea887..e9ed16a8e91 100644
--- a/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java
+++ b/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java
@@ -1,6 +1,6 @@
 public class test_insert_multiple
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder sb = new StringBuilder("ad");
       org.cprover.CProverString.insert(sb, 1, 'c');
diff --git a/jbmc/regression/jbmc-strings/java_insert_string/test.desc b/jbmc/regression/jbmc-strings/java_insert_string/test.desc
index 79fa2931c93..698c2b13e34 100644
--- a/jbmc/regression/jbmc-strings/java_insert_string/test.desc
+++ b/jbmc/regression/jbmc-strings/java_insert_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_string.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_insert_string.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java b/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java
index 50cd222f6ec..ad4d0894665 100644
--- a/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java
+++ b/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java
@@ -1,6 +1,6 @@
 public class test_insert_string
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder sb = new StringBuilder("ad");
       org.cprover.CProverString.insert(sb, 1, "bc");
diff --git a/jbmc/regression/jbmc/NondetCharSequence/test.desc b/jbmc/regression/jbmc/NondetCharSequence/test.desc
index baaa60614e5..0ef615186ed 100644
--- a/jbmc/regression/jbmc/NondetCharSequence/test.desc
+++ b/jbmc/regression/jbmc/NondetCharSequence/test.desc
@@ -1,6 +1,6 @@
 CORE
 NondetCharSequence.class
-
+--function NondetCharSequence.main
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc/NondetString/test.desc b/jbmc/regression/jbmc/NondetString/test.desc
index 6756c4a7630..d82c1b0b0c9 100644
--- a/jbmc/regression/jbmc/NondetString/test.desc
+++ b/jbmc/regression/jbmc/NondetString/test.desc
@@ -1,6 +1,6 @@
 CORE
 NondetString.class
-
+--function NondetString.main
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc/NondetStringBuffer/test.desc b/jbmc/regression/jbmc/NondetStringBuffer/test.desc
index 8c520b5f387..84ffb5ea110 100644
--- a/jbmc/regression/jbmc/NondetStringBuffer/test.desc
+++ b/jbmc/regression/jbmc/NondetStringBuffer/test.desc
@@ -1,6 +1,6 @@
 CORE
 NondetStringBuffer.class
-
+--function NondetStringBuffer.main
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc/NondetStringBuilder/test.desc b/jbmc/regression/jbmc/NondetStringBuilder/test.desc
index 6aa68c42d41..e0292b9769f 100644
--- a/jbmc/regression/jbmc/NondetStringBuilder/test.desc
+++ b/jbmc/regression/jbmc/NondetStringBuilder/test.desc
@@ -1,6 +1,6 @@
 CORE
 NondetStringBuilder.class
-
+--function NondetStringBuilder.main
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
index 778e1104824..0735ec2d46d 100644
--- a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
+++ b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
@@ -1,6 +1,6 @@
 CORE
 annotations.class
---verbosity 10 --show-symbol-table
+--verbosity 10 --show-symbol-table --function annotations.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations
diff --git a/jbmc/regression/jbmc/class-fields/test.desc b/jbmc/regression/jbmc/class-fields/test.desc
index abf3d4e911c..64eb85f6683 100644
--- a/jbmc/regression/jbmc/class-fields/test.desc
+++ b/jbmc/regression/jbmc/class-fields/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc/class-literals/test.desc b/jbmc/regression/jbmc/class-literals/test.desc
index de97168986e..a39e4029a74 100644
--- a/jbmc/regression/jbmc/class-literals/test.desc
+++ b/jbmc/regression/jbmc/class-literals/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/class-literals/test_lazy.desc b/jbmc/regression/jbmc/class-literals/test_lazy.desc
index c1e82a18b31..6cef52b953b 100644
--- a/jbmc/regression/jbmc/class-literals/test_lazy.desc
+++ b/jbmc/regression/jbmc/class-literals/test_lazy.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods
+--lazy-methods --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/classtest1/classtest1.class b/jbmc/regression/jbmc/classtest1/classtest1.class
index e105964df9121fbb37757e0c5c9d7aee43077022..4623a93e5417d3245dce5b5e0e0c8dd574f71ec6 100644
GIT binary patch
delta 11
Scmcc5bf0O$e@4zpjPU>+#RN_O

delta 11
Scmcc5bf0O$e@2c;jPU>+!30eJ

diff --git a/jbmc/regression/jbmc/classtest1/classtest1.java b/jbmc/regression/jbmc/classtest1/classtest1.java
index 532926c474d..82b2e804e66 100644
--- a/jbmc/regression/jbmc/classtest1/classtest1.java
+++ b/jbmc/regression/jbmc/classtest1/classtest1.java
@@ -1,6 +1,6 @@
 public class classtest1
 {
-  static void main(String[] args)
+  public static void main(String[] args)
   {
     g(classtest1.class);
   }
diff --git a/jbmc/regression/jbmc/exceptions23/test.desc b/jbmc/regression/jbmc/exceptions23/test.desc
index fd651101086..d9ccdcfc182 100644
--- a/jbmc/regression/jbmc/exceptions23/test.desc
+++ b/jbmc/regression/jbmc/exceptions23/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc/exceptions24/test.desc b/jbmc/regression/jbmc/exceptions24/test.desc
index 1bf09a500d5..523a3078bce 100644
--- a/jbmc/regression/jbmc/exceptions24/test.desc
+++ b/jbmc/regression/jbmc/exceptions24/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc/finally1/test.desc b/jbmc/regression/jbmc/finally1/test.desc
index a5fb4996899..9a6a879eae8 100644
--- a/jbmc/regression/jbmc/finally1/test.desc
+++ b/jbmc/regression/jbmc/finally1/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE
diff --git a/jbmc/regression/jbmc/finally2/test.desc b/jbmc/regression/jbmc/finally2/test.desc
index ae317e016fe..ae776b8ed1f 100644
--- a/jbmc/regression/jbmc/finally2/test.desc
+++ b/jbmc/regression/jbmc/finally2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE
diff --git a/jbmc/regression/jbmc/finally3/test.desc b/jbmc/regression/jbmc/finally3/test.desc
index 40c2fe0ab68..fb6be4be278 100644
--- a/jbmc/regression/jbmc/finally3/test.desc
+++ b/jbmc/regression/jbmc/finally3/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: SUCCESS
diff --git a/jbmc/regression/jbmc/finally4/test.desc b/jbmc/regression/jbmc/finally4/test.desc
index eeba95d006c..60ea3c4cb9e 100644
--- a/jbmc/regression/jbmc/finally4/test.desc
+++ b/jbmc/regression/jbmc/finally4/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 7: FAILURE
diff --git a/jbmc/regression/jbmc/finally5/test.desc b/jbmc/regression/jbmc/finally5/test.desc
index cc3b6780920..dcf21ec2d2d 100644
--- a/jbmc/regression/jbmc/finally5/test.desc
+++ b/jbmc/regression/jbmc/finally5/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: FAILURE
diff --git a/jbmc/regression/jbmc/finally6/test.desc b/jbmc/regression/jbmc/finally6/test.desc
index 91aca5d1b77..3a05a209373 100644
--- a/jbmc/regression/jbmc/finally6/test.desc
+++ b/jbmc/regression/jbmc/finally6/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 12: FAILURE
diff --git a/jbmc/regression/jbmc/finally7/test.desc b/jbmc/regression/jbmc/finally7/test.desc
index 5772f2dea33..27fd61ddad6 100644
--- a/jbmc/regression/jbmc/finally7/test.desc
+++ b/jbmc/regression/jbmc/finally7/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: SUCCESS
diff --git a/jbmc/regression/jbmc/jsr2/test.desc b/jbmc/regression/jbmc/jsr2/test.desc
index 844d0c49668..dc172cf106e 100644
--- a/jbmc/regression/jbmc/jsr2/test.desc
+++ b/jbmc/regression/jbmc/jsr2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 Labels: pc3
diff --git a/jbmc/regression/jbmc/method_parmeters1/method_parameters.class b/jbmc/regression/jbmc/method_parameters1/method_parameters.class
similarity index 100%
rename from jbmc/regression/jbmc/method_parmeters1/method_parameters.class
rename to jbmc/regression/jbmc/method_parameters1/method_parameters.class
diff --git a/jbmc/regression/jbmc/method_parmeters1/method_parameters.java b/jbmc/regression/jbmc/method_parameters1/method_parameters.java
similarity index 100%
rename from jbmc/regression/jbmc/method_parmeters1/method_parameters.java
rename to jbmc/regression/jbmc/method_parameters1/method_parameters.java
diff --git a/jbmc/regression/jbmc/method_parmeters1/test.desc b/jbmc/regression/jbmc/method_parameters1/test.desc
similarity index 100%
rename from jbmc/regression/jbmc/method_parmeters1/test.desc
rename to jbmc/regression/jbmc/method_parameters1/test.desc
diff --git a/jbmc/regression/jbmc/method_parmeters2/method_parameters.class b/jbmc/regression/jbmc/method_parameters2/method_parameters.class
similarity index 100%
rename from jbmc/regression/jbmc/method_parmeters2/method_parameters.class
rename to jbmc/regression/jbmc/method_parameters2/method_parameters.class
diff --git a/jbmc/regression/jbmc/method_parmeters2/method_parameters.java b/jbmc/regression/jbmc/method_parameters2/method_parameters.java
similarity index 100%
rename from jbmc/regression/jbmc/method_parmeters2/method_parameters.java
rename to jbmc/regression/jbmc/method_parameters2/method_parameters.java
diff --git a/jbmc/regression/jbmc/method_parmeters2/test.desc b/jbmc/regression/jbmc/method_parameters2/test.desc
similarity index 100%
rename from jbmc/regression/jbmc/method_parmeters2/test.desc
rename to jbmc/regression/jbmc/method_parameters2/test.desc
diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc
index 49668103f1f..145c918788c 100644
--- a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc
+++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 12 function .* bytecode-index 15: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc
index 49668103f1f..145c918788c 100644
--- a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc
+++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 12 function .* bytecode-index 15: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring
diff --git a/jbmc/regression/strings-smoke-tests/java_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_char_at/test.desc
index 5279f32726e..1b0d5054458 100644
--- a/jbmc/regression/strings-smoke-tests/java_char_at/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_char_at.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_char_at.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_char_at/test_char_at.java b/jbmc/regression/strings-smoke-tests/java_char_at/test_char_at.java
index c91fc7d1cff..7ac598b83f4 100644
--- a/jbmc/regression/strings-smoke-tests/java_char_at/test_char_at.java
+++ b/jbmc/regression/strings-smoke-tests/java_char_at/test_char_at.java
@@ -1,6 +1,6 @@
 public class test_char_at {
 
-  public static void main(/*String[] argv*/) {
+  public static void main() {
     String s = new String("abc");
     assert(org.cprover.CProverString.charAt(s, 2)=='c');
   }
diff --git a/jbmc/regression/strings-smoke-tests/java_code_point/test.desc b/jbmc/regression/strings-smoke-tests/java_code_point/test.desc
index 2c3def77c28..31a1a0340e4 100644
--- a/jbmc/regression/strings-smoke-tests/java_code_point/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_code_point/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_code_point.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_code_point.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_code_point/test_code_point.java b/jbmc/regression/strings-smoke-tests/java_code_point/test_code_point.java
index ae782ecddfa..dc18dab2853 100644
--- a/jbmc/regression/strings-smoke-tests/java_code_point/test_code_point.java
+++ b/jbmc/regression/strings-smoke-tests/java_code_point/test_code_point.java
@@ -1,6 +1,6 @@
 public class test_code_point
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = "!𐤇𐤄𐤋𐤋𐤅";
       assert(org.cprover.CProverString.codePointAt(s, 1) == 67847);
diff --git a/jbmc/regression/strings-smoke-tests/java_contains/test.desc b/jbmc/regression/strings-smoke-tests/java_contains/test.desc
index a0b0afc6933..45af4256612 100644
--- a/jbmc/regression/strings-smoke-tests/java_contains/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_contains/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_contains.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function test_contains.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc b/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc
index 2c0d8942b68..e8b0e0c7c24 100644
--- a/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc
+++ b/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 test_contains.class
---refine-strings --verbosity 10 --string-max-length 100 --string-printable
+--refine-strings --verbosity 10 --string-max-length 100 --string-printable --function test_contains.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
index 91710ffcf63..4f3d210102a 100644
--- a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete_char_at.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_delete_char_at.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java
index 2c56fb54b44..3121aab316c 100644
--- a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java
+++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java
@@ -1,6 +1,6 @@
 public class test_delete_char_at
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder s = new StringBuilder();
       s.append("Abc");
diff --git a/jbmc/regression/strings-smoke-tests/java_endswith/test.desc b/jbmc/regression/strings-smoke-tests/java_endswith/test.desc
index 2dec4153ff7..4e04e6544ee 100644
--- a/jbmc/regression/strings-smoke-tests/java_endswith/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_endswith/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_endswith.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function test_endswith.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_endswith/test_endswith.java b/jbmc/regression/strings-smoke-tests/java_endswith/test_endswith.java
index f7729ef6a40..6d7ac2191d1 100644
--- a/jbmc/regression/strings-smoke-tests/java_endswith/test_endswith.java
+++ b/jbmc/regression/strings-smoke-tests/java_endswith/test_endswith.java
@@ -1,6 +1,6 @@
 public class test_endswith
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Abcd");
       String suff = "cd";
diff --git a/jbmc/regression/strings-smoke-tests/java_float/test.desc b/jbmc/regression/strings-smoke-tests/java_float/test.desc
index e9df3330ee1..c0a002b0ede 100644
--- a/jbmc/regression/strings-smoke-tests/java_float/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_float/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test_float.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_float.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_float/test_float.java b/jbmc/regression/strings-smoke-tests/java_float/test_float.java
index d2791d5c343..1e7e78d50c3 100644
--- a/jbmc/regression/strings-smoke-tests/java_float/test_float.java
+++ b/jbmc/regression/strings-smoke-tests/java_float/test_float.java
@@ -1,6 +1,6 @@
 public class test_float
 {
-   public static void main(/*String[] arg*/)
+   public static void main()
    {
       float inf = 100.0f / 0.0f;
       float minus_inf = -100.0f / 0.0f;
diff --git a/jbmc/regression/strings-smoke-tests/java_format/test.desc b/jbmc/regression/strings-smoke-tests/java_format/test.desc
index e688c95b140..e8e8666c160 100644
--- a/jbmc/regression/strings-smoke-tests/java_format/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_format/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --verbosity 10 --string-max-length 20
+--refine-strings --verbosity 10 --string-max-length 20 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_format2/test.desc b/jbmc/regression/strings-smoke-tests/java_format2/test.desc
index 0ea5e37ca19..f81c6fa17e1 100644
--- a/jbmc/regression/strings-smoke-tests/java_format2/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_format2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --verbosity 10 --string-max-length 20
+--refine-strings --verbosity 10 --string-max-length 20 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_format3/test.desc b/jbmc/regression/strings-smoke-tests/java_format3/test.desc
index 5aeac5fb776..e0a0de54aa4 100644
--- a/jbmc/regression/strings-smoke-tests/java_format3/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_format3/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --verbosity 10 --string-max-length 20
+--refine-strings --verbosity 10 --string-max-length 20 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc b/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc
index 54d6734c0ba..1392b360f66 100644
--- a/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_hash_code.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_hash_code.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_hash_code/test_hash_code.java b/jbmc/regression/strings-smoke-tests/java_hash_code/test_hash_code.java
index d9f42b7ff9d..04c33087e49 100644
--- a/jbmc/regression/strings-smoke-tests/java_hash_code/test_hash_code.java
+++ b/jbmc/regression/strings-smoke-tests/java_hash_code/test_hash_code.java
@@ -1,6 +1,6 @@
 public class test_hash_code
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s1 = "ab";
       String s2 = "ab";
diff --git a/jbmc/regression/strings-smoke-tests/java_if/test.desc b/jbmc/regression/strings-smoke-tests/java_if/test.desc
index a652d884b11..635e7c094cd 100644
--- a/jbmc/regression/strings-smoke-tests/java_if/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_if/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 11.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_index_of/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of/test.desc
index e5b6c994424..6fd524b72c1 100644
--- a/jbmc/regression/strings-smoke-tests/java_index_of/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_index_of/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_index_of/test_index_of.java b/jbmc/regression/strings-smoke-tests/java_index_of/test_index_of.java
index 3568dab9696..d5d9a766b66 100644
--- a/jbmc/regression/strings-smoke-tests/java_index_of/test_index_of.java
+++ b/jbmc/regression/strings-smoke-tests/java_index_of/test_index_of.java
@@ -1,6 +1,6 @@
 public class test_index_of
 {
-    public static void main(/*String[] argv*/)
+    public static void main()
     {
         String s = "Abc";
         String bc = "bc";
diff --git a/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc
index a3744c3a776..954e794efde 100644
--- a/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of2.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc
index c457e8cd7d0..30ce1a9a702 100644
--- a/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc
@@ -1,10 +1,8 @@
 CORE
 test_index_of_char.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of_char.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 non equal types
---
-Issue: cbmc/test-gen#77
diff --git a/jbmc/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java b/jbmc/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java
index 6a5d3d60bd6..ea395edc9f2 100644
--- a/jbmc/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java
+++ b/jbmc/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java
@@ -1,6 +1,6 @@
 public class test_index_of_char
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = "Abc";
       char c = 'c';
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc
index 3281b3d629b..bcae9bf0ea6 100644
--- a/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---refine-strings --verbosity 10  --string-max-length 1000
+--refine-strings --verbosity 10  --string-max-length 1000 --function test_insert_char.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java b/jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java
index 940292296f1..068b0ab5acc 100644
--- a/jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java
+++ b/jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java
@@ -1,6 +1,6 @@
 public class test_insert_char
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder sb = new StringBuilder("ac");
       org.cprover.CProverString.insert(sb, 1, 'b');
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc
index 5b77efb0d46..d36dc796a31 100644
--- a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_multiple.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_multiple.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java
index b505e24020e..c74177eda80 100644
--- a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java
+++ b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java
@@ -1,6 +1,6 @@
 public class test_insert_multiple
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder sb = new StringBuilder("ad");
       org.cprover.CProverString.insert(sb, 1, 'c');
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc
index 93596bf62ac..066e26a74b2 100644
--- a/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_string.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_string.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_string/test_insert_string.java b/jbmc/regression/strings-smoke-tests/java_insert_string/test_insert_string.java
index 547b89ae569..9053fa97d9d 100644
--- a/jbmc/regression/strings-smoke-tests/java_insert_string/test_insert_string.java
+++ b/jbmc/regression/strings-smoke-tests/java_insert_string/test_insert_string.java
@@ -1,6 +1,6 @@
 public class test_insert_string
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder sb = new StringBuilder("ad");
       org.cprover.CProverString.insert(sb, 1, "bc");
diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test.desc b/jbmc/regression/strings-smoke-tests/java_intern/test.desc
index 05b26307bb2..778cfffeae4 100644
--- a/jbmc/regression/strings-smoke-tests/java_intern/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_intern/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_intern.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_intern.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java b/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java
index 7f9d5283597..b8abb9f1f2c 100644
--- a/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java
+++ b/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java
@@ -1,6 +1,6 @@
 public class test_intern
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s1 = "abc";
       String s3 = "abc";
diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc b/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc
index 9fd0a299a7c..917218b59dd 100644
--- a/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_last_index_of.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_last_index_of.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java b/jbmc/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java
index 59b9f5ab36d..c4aecdfc718 100644
--- a/jbmc/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java
+++ b/jbmc/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java
@@ -1,6 +1,6 @@
 public class test_last_index_of
 {
-    public static void main(/*String[] argv*/)
+    public static void main()
     {
         String s = "abcab";
         String ab = "ab";
diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc
index a1ddc2cf440..451966cbac1 100644
--- a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_last_index_of_char.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_last_index_of_char.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java
index 029d59c9d68..fec963b8bf2 100644
--- a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java
+++ b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java
@@ -1,6 +1,6 @@
 public class test_last_index_of_char
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = "abcab";
       int n = s.lastIndexOf('a');
diff --git a/jbmc/regression/strings-smoke-tests/java_length/test.desc b/jbmc/regression/strings-smoke-tests/java_length/test.desc
index 59184450019..f3a7b3e99c7 100644
--- a/jbmc/regression/strings-smoke-tests/java_length/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_length/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_length.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_length.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/strings-smoke-tests/java_length/test_length.java b/jbmc/regression/strings-smoke-tests/java_length/test_length.java
index 620bdc448e9..ce844e67ea7 100644
--- a/jbmc/regression/strings-smoke-tests/java_length/test_length.java
+++ b/jbmc/regression/strings-smoke-tests/java_length/test_length.java
@@ -1,6 +1,6 @@
 public class test_length
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Abc");
       int l = s.length();
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc
index f95b66184a8..4f888659004 100644
--- a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc
+++ b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* FAILURE$
diff --git a/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc b/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc
index ba11fa1f7e5..cae6c9a525b 100644
--- a/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_replace_char.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_replace_char.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_replace_char/test_replace_char.java b/jbmc/regression/strings-smoke-tests/java_replace_char/test_replace_char.java
index 82a023924e2..0059c309ebe 100644
--- a/jbmc/regression/strings-smoke-tests/java_replace_char/test_replace_char.java
+++ b/jbmc/regression/strings-smoke-tests/java_replace_char/test_replace_char.java
@@ -1,6 +1,6 @@
 public class test_replace_char
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("abcabd");
       String t = s.replace('b','m');
diff --git a/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc
index bfb3be131a5..0adb430c3b3 100644
--- a/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_set_char_at.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_set_char_at.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java b/jbmc/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
index 9e67eba0de7..7151c9ba177 100644
--- a/jbmc/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
+++ b/jbmc/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
@@ -1,6 +1,6 @@
 public class test_set_char_at
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Abc");
       char c = org.cprover.CProverString.charAt(s, 1);
diff --git a/jbmc/regression/strings-smoke-tests/java_set_length/test.desc b/jbmc/regression/strings-smoke-tests/java_set_length/test.desc
index 92b178f222a..21dd8d95a49 100644
--- a/jbmc/regression/strings-smoke-tests/java_set_length/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_set_length/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_set_length.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function test_set_length.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java b/jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java
index 5894b27beeb..37c60a9912a 100644
--- a/jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java
+++ b/jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java
@@ -1,6 +1,6 @@
 public class test_set_length
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder s = new StringBuilder("abc");
       s.setLength(10);
diff --git a/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc b/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc
index 96348e08f11..5a0ca5ea703 100644
--- a/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_starts_with.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_starts_with.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_starts_with/test_starts_with.java b/jbmc/regression/strings-smoke-tests/java_starts_with/test_starts_with.java
index aba79d846c0..def31ed6709 100644
--- a/jbmc/regression/strings-smoke-tests/java_starts_with/test_starts_with.java
+++ b/jbmc/regression/strings-smoke-tests/java_starts_with/test_starts_with.java
@@ -1,6 +1,6 @@
 public class test_starts_with
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Abcd");
       String pref = "Ab";
diff --git a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc
index 8fbbb04690c..2debae07cf9 100644
--- a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_sb_length.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_sb_length.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java
index b616749ffb4..e09d8807949 100644
--- a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java
+++ b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java
@@ -1,6 +1,6 @@
 public class test_sb_length
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder x = new StringBuilder("abc");
       x.append("de");
diff --git a/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc b/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc
index b0949a841ea..e16da196007 100644
--- a/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_subsequence.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_subsequence.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_subsequence/test_subsequence.java b/jbmc/regression/strings-smoke-tests/java_subsequence/test_subsequence.java
index 6fdc3e6735e..0a6c18176da 100644
--- a/jbmc/regression/strings-smoke-tests/java_subsequence/test_subsequence.java
+++ b/jbmc/regression/strings-smoke-tests/java_subsequence/test_subsequence.java
@@ -1,6 +1,6 @@
 public class test_subsequence
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String abcdef = "AbcDef";
       CharSequence cde = org.cprover.CProverString.subSequence(abcdef,2,5);
diff --git a/jbmc/regression/strings-smoke-tests/java_substring/test.desc b/jbmc/regression/strings-smoke-tests/java_substring/test.desc
index 762b0237086..5787d80275d 100644
--- a/jbmc/regression/strings-smoke-tests/java_substring/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_substring/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_substring.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_substring.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_substring/test_substring.java b/jbmc/regression/strings-smoke-tests/java_substring/test_substring.java
index e94ee9c51cb..88278f455b9 100644
--- a/jbmc/regression/strings-smoke-tests/java_substring/test_substring.java
+++ b/jbmc/regression/strings-smoke-tests/java_substring/test_substring.java
@@ -1,6 +1,6 @@
 public class test_substring
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String abcdef = "AbcDef";
       String cde = org.cprover.CProverString.substring(abcdef, 2,5);
diff --git a/jbmc/regression/strings-smoke-tests/java_trim/test.desc b/jbmc/regression/strings-smoke-tests/java_trim/test.desc
index 94142169895..d60e82f050e 100644
--- a/jbmc/regression/strings-smoke-tests/java_trim/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_trim/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_trim.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function test_trim.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_trim/test_trim.java b/jbmc/regression/strings-smoke-tests/java_trim/test_trim.java
index 20dd7ba2796..679a0f821e9 100644
--- a/jbmc/regression/strings-smoke-tests/java_trim/test_trim.java
+++ b/jbmc/regression/strings-smoke-tests/java_trim/test_trim.java
@@ -1,6 +1,6 @@
 public class test_trim
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String empty = "   ";
       assert(empty.trim().isEmpty());
diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/Test.class b/jbmc/regression/strings-smoke-tests/max_input_length/Test.class
index 37d68870ec961e859c4aefbab310cfa3ae28ac2a..d07682d2cf6482c75a529491af2d6b29c0327411 100644
GIT binary patch
delta 58
zcmeBX?PuNaicvg*fti7cfq_A7Hv?0o5c75h79Xu+3{sQ-GU^J6GjKAfGH@}70OdIt
N82>P+PPSq42LNUS3ljhU

delta 54
zcmeBY?PlHZicvU(fti7cfq_A3Hv?0o5c75h7N5zCOu9nC44e##3|tH%KsgQu#y<>-
IlO34+0ThP_`Tzg`

diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/Test.java b/jbmc/regression/strings-smoke-tests/max_input_length/Test.java
index 9c6e8839f58..308da33a348 100644
--- a/jbmc/regression/strings-smoke-tests/max_input_length/Test.java
+++ b/jbmc/regression/strings-smoke-tests/max_input_length/Test.java
@@ -3,7 +3,7 @@ public static void main(String s) {
         // This prevent anything from happening if we were to add a constraints on strings
         // being smaller than 40
         String t = new String("0123456789012345678901234567890123456789");
-	if (s.length() >= 30)
+	if (s != null && s.length() >= 30)
 	    // This should not happen when string-max-input length is smaller
 	    // than 30
 	    assert false;
diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc b/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc
index c5252f6c564..0943fca690c 100644
--- a/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc
+++ b/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --verbosity 10 --string-max-length 45  --string-max-input-length 31
+--refine-strings --verbosity 10 --string-max-length 45  --string-max-input-length 31 --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc b/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc
index 0edaf226ccc..307bc7db2fc 100644
--- a/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc
+++ b/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20
+--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20 --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

From 3cb8bcf634e58e346828d9ed32f151dd43f9677f Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 10 Jun 2018 18:03:02 +0100
Subject: [PATCH 9/9] Deduplicate string tests

---
 .../jbmc-strings/java_append_string/test.desc |   7 ----
 .../test_append_string.class                  | Bin 1032 -> 0 bytes
 .../test_append_string.java                   |  14 --------
 .../jbmc-strings/java_case/test.desc          |   7 ----
 .../jbmc-strings/java_case/test_case.class    | Bin 839 -> 0 bytes
 .../jbmc-strings/java_case/test_case.java     |  12 -------
 .../jbmc-strings/java_char_array/test.desc    |   7 ----
 .../java_char_array/test_char_array.class     | Bin 676 -> 0 bytes
 .../java_char_array/test_char_array.java      |  13 --------
 .../jbmc-strings/java_code_point/test.desc    |   7 ----
 .../java_code_point/test_code_point.class     | Bin 941 -> 0 bytes
 .../java_code_point/test_code_point.java      |  14 --------
 .../jbmc-strings/java_contains/test.desc      |   7 ----
 .../java_contains/test_contains.class         | Bin 671 -> 0 bytes
 .../java_contains/test_contains.java          |   9 ------
 .../java_delete_char_at/test.desc             |   7 ----
 .../test_delete_char_at.class                 | Bin 923 -> 0 bytes
 .../test_delete_char_at.java                  |  11 -------
 .../jbmc-strings/java_endswith/test.desc      |   7 ----
 .../java_endswith/test_endswith.class         | Bin 666 -> 0 bytes
 .../java_endswith/test_endswith.java          |   9 ------
 .../jbmc-strings/java_equal/test.desc         |   7 ----
 .../jbmc-strings/java_equal/test_equal.class  | Bin 725 -> 0 bytes
 .../jbmc-strings/java_equal/test_equal.java   |   9 ------
 .../jbmc-strings/java_float/test.desc         |   7 ----
 .../jbmc-strings/java_float/test_float.class  | Bin 1015 -> 0 bytes
 .../jbmc-strings/java_float/test_float.java   |  17 ----------
 .../jbmc-strings/java_hash_code/test.desc     |   7 ----
 .../java_hash_code/test_hash_code.class       | Bin 602 -> 0 bytes
 .../java_hash_code/test_hash_code.java        |   9 ------
 .../jbmc-strings/java_index_of/test.desc      |   7 ----
 .../java_index_of/test_index_of.class         | Bin 631 -> 0 bytes
 .../java_index_of/test_index_of.java          |  10 ------
 .../jbmc-strings/java_index_of_char/test.desc |   7 ----
 .../test_index_of_char.class                  | Bin 614 -> 0 bytes
 .../test_index_of_char.java                   |  10 ------
 .../java_insert_char_array/test.desc          |   8 -----
 .../test_insert_char_array.class              | Bin 1416 -> 0 bytes
 .../test_insert_char_array.java               |  30 ------------------
 .../java_insert_multiple/test.desc            |   7 ----
 .../test_insert_multiple.class                | Bin 979 -> 0 bytes
 .../test_insert_multiple.java                 |  11 -------
 .../jbmc-strings/java_insert_string/test.desc |   7 ----
 .../test_insert_string.class                  | Bin 897 -> 0 bytes
 .../test_insert_string.java                   |  10 ------
 .../java_append_object/test.desc              |  10 ------
 .../test_append_object.class                  | Bin 992 -> 0 bytes
 .../test_append_object.java                   |  17 ----------
 .../java_char_array_init/test.desc            |  10 ------
 .../java_char_array_init/test_init.class      | Bin 1046 -> 0 bytes
 .../java_char_array_init/test_init.java       |  21 ------------
 .../java_compare/test.desc                    |   8 -----
 .../java_compare/test_compare.class           | Bin 623 -> 0 bytes
 .../java_compare/test_compare.java            |   9 ------
 .../strings-smoke-tests/java_concat/test.desc |   9 ------
 .../java_concat/test_concat.class             | Bin 847 -> 0 bytes
 .../java_concat/test_concat.java              |  13 --------
 .../strings-smoke-tests/java_delete/test.desc |   8 -----
 .../java_delete/test_delete.class             | Bin 856 -> 0 bytes
 .../java_delete/test_delete.java              |  10 ------
 .../strings-smoke-tests/java_empty/test.desc  |   8 -----
 .../java_empty/test_empty.class               | Bin 571 -> 0 bytes
 .../java_empty/test_empty.java                |   8 -----
 .../java_insert_int/test.desc                 |   8 -----
 .../java_insert_int/test_insert_int.class     | Bin 866 -> 0 bytes
 .../java_insert_int/test_insert_int.java      |  10 ------
 66 files changed, 443 deletions(-)
 delete mode 100644 jbmc/regression/jbmc-strings/java_append_string/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_append_string/test_append_string.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_append_string/test_append_string.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_case/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_case/test_case.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_case/test_case.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_char_array/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_char_array/test_char_array.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_char_array/test_char_array.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_code_point/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_code_point/test_code_point.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_code_point/test_code_point.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_contains/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_contains/test_contains.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_contains/test_contains.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_delete_char_at/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_endswith/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_endswith/test_endswith.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_endswith/test_endswith.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_equal/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_equal/test_equal.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_equal/test_equal.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_float/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_float/test_float.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_float/test_float.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_hash_code/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_index_of/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_index_of/test_index_of.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_index_of/test_index_of.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_index_of_char/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_char_array/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_multiple/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_string/test.desc
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.class
 delete mode 100644 jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_append_object/test.desc
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.class
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.java
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_char_array_init/test.desc
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.class
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.java
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_compare/test.desc
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_compare/test_compare.class
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_compare/test_compare.java
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_concat/test.desc
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_concat/test_concat.class
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_concat/test_concat.java
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete/test.desc
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete/test_delete.class
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete/test_delete.java
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_empty/test.desc
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_empty/test_empty.class
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_empty/test_empty.java
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_insert_int/test.desc
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.class
 delete mode 100644 jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.java

diff --git a/jbmc/regression/jbmc-strings/java_append_string/test.desc b/jbmc/regression/jbmc-strings/java_append_string/test.desc
deleted file mode 100644
index cb881ab83d9..00000000000
--- a/jbmc/regression/jbmc-strings/java_append_string/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-FUTURE
-test_append_string.class
---refine-strings --string-max-length 1000
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion.1\].* line 12.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_append_string/test_append_string.class b/jbmc/regression/jbmc-strings/java_append_string/test_append_string.class
deleted file mode 100644
index f2cb5cf8bea64858805fef9f4a7b85663a237736..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1032
zcmZ`%YfsZq7=F%f?Meru444;G5OFYIiYO|G+zkq9GNXYnq^xJ;VAsyJGx3j@$RF^t
zm~4q8`rRKzd{4(%Ci<c8dHdd;=e_(s{qYmPES_n|U_`-96{8v=xTRoBLmVSg+*XlG
zVjL41@|cvCDXC2-VW6Pmj!d|#U`9h)*0`rp!TSmxF!YU@zR$ftxQ@Rjd~@IC76aR5
zNGu3P1d9yO-1u9D*s5!BhMq0q@Rzm9KKI_pU~*JU;V`6%fmwRLZB|1w@g#l>>O#pr
zE29<Nnpff*LM9Cc+z<B5YLz?Io*#I^IhZ~)KbkrQk!46ry<nTpL7^Br86uXD&N<5c
z+qqH`w#7Xi5Alcs%Vh<Rb<ATy!4n;ec&cLw%Tk-u(T@S*Y>9GN#|l;%vh8xqtx>Fd
zp6f9f7g;J;)3J_?4vw$(4|yqI=+AAni#3VQ%h@HGjWSIAE8s%TSwHg~7{yP1z$>&3
zw<eLANy06>rr8CA#mx#O^o97HW(K7ygKXMT2g4@qkf9p5twCpU;};lF<plpwGj0Dr
zCFovy+O4nJbW{uj7Wak6t@E+ci3Bxr&_(THm~Jyer_It?xfIf(pyeV<@)G?G(aY$K
zPc*>3$v|8tnFx&xNnAM({Y<G*@;yI6WXFg$5PNZg_)Y_ft^7nC%DcRw%I6r#d>tBn
zUE8Ej)}bFGb%e~M(OpN+7j&H<O=-QqBwi%M8zUql0gaFiD1@ovI@!j^l1CS2pkos$
zT&1XPuv2U*7*cSJWEk0MXEx*w^cqGTeMeAYUlEIbN2(3gYE71kBcd<K0o<UU2!{Uv
D<SE~p

diff --git a/jbmc/regression/jbmc-strings/java_append_string/test_append_string.java b/jbmc/regression/jbmc-strings/java_append_string/test_append_string.java
deleted file mode 100644
index 54665da29cc..00000000000
--- a/jbmc/regression/jbmc-strings/java_append_string/test_append_string.java
+++ /dev/null
@@ -1,14 +0,0 @@
-public class test_append_string
-{
-   public static void main(/*String[] args*/)
-   {
-      String di = new String("di");
-      StringBuilder diff = new StringBuilder();
-      diff.append(di);
-      diff.append("ff");
-      System.out.println(diff);
-      String s = diff.toString();
-      System.out.println(s);
-      assert (!s.equals("diff"));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_case/test.desc b/jbmc/regression/jbmc-strings/java_case/test.desc
deleted file mode 100644
index b194d77cd40..00000000000
--- a/jbmc/regression/jbmc-strings/java_case/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_case.class
---refine-strings --string-max-length 1000 --function test_case.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 8.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_case/test_case.class b/jbmc/regression/jbmc-strings/java_case/test_case.class
deleted file mode 100644
index 5887b496986fb7f563de13bd3e40911264f14773..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 839
zcmZuvYi|-k6g|Uhmt}cvq2dFzwIa}3d{AF~#1=I%QvHCMv|r2s6S9@=;_jmV!2i(x
z0Y9q=BsS6S{;0+~y8`i%Ozzy7bLO6NXXfYWx9<Szc%UJRiwZ8OxU3<B1sN7)xDrPi
zODe9)MM=dq6=j)L6jU`N<)LK_E4Z#;m0@m)yRL9N)3)44rpw!X(Pd!!46zN<GQBN^
zaJllDA=0qBf+5{BE%AJK*cQ%9NhaWsn-)W|<?+tjT|V%)$ryvW(dqxLp|$Lx(-BWh
zc_QTr*L&09u2?<b@41c~@(dZ7*ZSP*)moloT0Mr)c3Xlq9XD`O$1NEQ%n`r|xQ)7`
z?8xPgjy2q2D9nm%Px^Z7IJUzOpQ<XjtK%N-|DpM!eIPm>L%!Uc)d-BN%l;Fd-LyXl
zr$M$Ea^=duG@tZpFqn{H;@yz<-M?xELhBW};!Hqz+Oup&1cm=APt^3xRHIK%#xUO%
zuIY&Gv`=~fZ%6>W*FF~L6J+V9uuMT-8D(LRZR9D=)2c`_qd8g~gMF4noS_)=H|era
zm{LE|(J*0KCkX8s;V~l5sv|_36k@wypd6#LY^Wo|k5F7OG(X8zjl>B05fUdz?v0W9
zAvHq2#v)Y8qtHk#4TVgpD3M}~cGf80L;`1tkper#rh;?9AmseiQ{DFoWR3I)nPVuC
ZPl$xSLYc`-T9Kuq2<Z=H!xwxP#b52Br6K?T

diff --git a/jbmc/regression/jbmc-strings/java_case/test_case.java b/jbmc/regression/jbmc-strings/java_case/test_case.java
deleted file mode 100644
index ec66e5ed395..00000000000
--- a/jbmc/regression/jbmc-strings/java_case/test_case.java
+++ /dev/null
@@ -1,12 +0,0 @@
-public class test_case
-{
-   public static void main()
-   {
-      String s = new String("Ab");
-      String l = s.toLowerCase();
-      String u = s.toUpperCase();
-      assert(!l.equals("ab") ||
-             !u.equals("AB") ||
-             !s.equalsIgnoreCase("aB"));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_char_array/test.desc b/jbmc/regression/jbmc-strings/java_char_array/test.desc
deleted file mode 100644
index 4cfdbf58a28..00000000000
--- a/jbmc/regression/jbmc-strings/java_char_array/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_char_array.class
---refine-strings --string-max-length 1000 --function test_char_array.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 9.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.class b/jbmc/regression/jbmc-strings/java_char_array/test_char_array.class
deleted file mode 100644
index 38a7ecf41eddf662574382383851643fa631b055..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 676
zcmZ9JO>fgc5Qg9J*E){dIB97^X@Ek3d>|@8j-?_BAR$UQ1R+rl)yA=kOKPLFQ;EOQ
zQ*N9ADV0DfcYYKw8_`5?+1>ei=b71`zrLLVXydL24^<bJJ*?r1KGq9xQ4_f8!9i8v
znuqJy5V%2D+LT!qsXR`T>~WmQ{xBL4XrJJ0$4Q*;5X^exHNonpgNRVtjgx3^bli{B
zE1k@NV;Lueg<dYh_b=p!saxQtz$U@n4u^kbyk0s|Ve~ZCMay}V<p<$AsSc!4^5eZD
zc_Mu*V3GUDe#rGcZsE3%JE;38!Y5R9&el*Shg+Qs<|j&}imCpS6KMEoqD2ViMKAkD
zQJDYZ>g6g<4hhEFE}@vGT?XoC9v-XS&`w7)cDTx_KWngEn(K9kygI_lAj)DD4Q5Qd
zh<wBW-rGJlc=H~A3k6j@1;0%2varZ!iLDyn#JAl%1AW$s2>5iSPC^0YS?UQ4SR8v$
zF`hRkFn3#a`(e|Zz}oo&`xLd-xiiLUEs$fB*Mo43;&(W2&LDnhVPh)1#?su4DI6vf
zOyr`%ZSM1{!jUrQHyf6~lE5-)G#8g<4DBfwr&Zhu3a1d(Cs^iJ*z*n-=vvK&;Xl#?
JuCQTX^$$Dod?f$?

diff --git a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java b/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java
deleted file mode 100644
index 5028f5afa4d..00000000000
--- a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java
+++ /dev/null
@@ -1,13 +0,0 @@
-public class test_char_array
-{
-   public static void main()
-   {
-      String s = "abc";
-      char [] str = s.toCharArray();
-      char c = str[2];
-      char a = s.charAt(0);
-      assert(str.length != 3 ||
-             a != 'a' ||
-             c != 'c');
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_code_point/test.desc b/jbmc/regression/jbmc-strings/java_code_point/test.desc
deleted file mode 100644
index cda7f110aba..00000000000
--- a/jbmc/regression/jbmc-strings/java_code_point/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_code_point.class
---refine-strings --string-max-length 1000 --function test_code_point.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 8.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.class b/jbmc/regression/jbmc-strings/java_code_point/test_code_point.class
deleted file mode 100644
index f2f5fbad63a60c992bb2f3c9ef2d15fb99700de0..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 941
zcmZ8fOHUI~7(KV0>20S|C<8)Okb<aXK<cBS2oh-3ga~SaU}Qsv_JV_DrkR<VxHTFV
z{sUGJ7p{GzB$DW!|H4nu_}$UA;^xeqbI*6a*FF06?K^-1W;Gbd#xcY(tRaeQ6fD8z
z>3jldjA*!kixMtL$VnKLU`mO}F{YsdS&nfHmodSSXXqZWd|!Bh?K=Kl+qX8VqQbz|
z7-BQFV+XSg(cI`NgHm!Uf}wNKcErQ_&W7-wNHJaPShmBES`Mu8izTZT(i~T)MuzxI
zx%$^eTXySSS=_f}P){KIV7*M1>owPQf{AVGrKRH(dKm_Xj`v<4e|;C?n-JgsgKru7
zq&i=<oUQzF;MvYrv2Ir@!qagT*K~BFhw|&Vj)IOG5+-p|$1Mp{xXqAh$Imyrzvp?b
zNB#X*7{|1Z8Qft=w}T#SY>RSmg8EYj#ap$Sa4K?Gk7Z*F{ketF#dhq8f~OghatNVx
zp2P}?7s#bW7R9FP(ZD)dOv$ZFTQ#>3N)2~&(-%SURV$@WyDLApyry4?{Mz|TRa!Vh
zZ$<dFCn~M}X?;PRE@<0p7^2r?(34~7jGQK&=%vZ+5cbjE0DT#KRr3JslN2ID7z;^;
z1Wvc4A1E|JcdJI^!6Bm04xlWK8EONur=P)hF=r|b#0_;1lV+@egglL#O1uG0-N&%0
zkTe<FM@H)Ov1kLSJtPm&K~9}NWbR0q+k{4Em9oW<1gG-j7@<n?#7_}ZgpMWRR*=FO
zQYOKEVuj-@M?cX6t%3_-6F`@dZlG%yT=@tk`USk5tJ$aYQ4!JS<TTEOr40TCo#V>@

diff --git a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java b/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java
deleted file mode 100644
index 266a05c1646..00000000000
--- a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java
+++ /dev/null
@@ -1,14 +0,0 @@
-public class test_code_point
-{
-   public static void main()
-   {
-      String s = "!𐤇𐤄𐤋𐤋𐤅";
-      StringBuilder sb = new StringBuilder();
-      sb.appendCodePoint(0x10907);
-      assert(s.codePointAt(1) != 67847 ||
-             s.codePointBefore(3) != 67847 ||
-             s.codePointCount(1,5) < 2 ||
-             s.offsetByCodePoints(1,2) < 3  ||
-             s.charAt(1) != sb.charAt(0));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_contains/test.desc b/jbmc/regression/jbmc-strings/java_contains/test.desc
deleted file mode 100644
index cfa99b27ba0..00000000000
--- a/jbmc/regression/jbmc-strings/java_contains/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_contains.class
---refine-strings --string-max-length 1000 --function test_contains.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 7.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_contains/test_contains.class b/jbmc/regression/jbmc-strings/java_contains/test_contains.class
deleted file mode 100644
index 9bbccb03775ac6ea7b4ea53619317d2a13ed93aa..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 671
zcmY*XT~8B16g_vl-Q8{%TegB#L`90WC6O22AVgC2#i|cACgsIUw-a0_yE;4dzrY{h
zSxsmniN5onG~QWlE6HT$&iy#&+&gpi`}+?7+t~CG;I@l99#(u<xa(oH1RwXz<-Ust
zK0Fg&^YIYtE*gYdLu8p$I!=@9S)7T%NDc{fKyY^BB-VR`LbLUbV0Y4?BviU_B43YB
z22#B>$s9NlaY9(=X%QX25+8FnYan>L(dZwB-%H0Tk}qOY5o(#~_feW?uFResiO(WH
z1yw@T*jpo!9B%crijzZT-ycLKx<RmvwSXG|9^o;eK2P4C_V8S(RI!+A3@(}hT4-Ox
ze=|6ektQrPyK|hsq&ucxZ>o>5@_$O_gHS#BX)KdS?zDJLm3et*#KR;k4`miBIh?8D
z(daP;c#;QL;|B@&xu{w<&9GGfqoB(BBHvc|BtDDn3FwPSM9907I|(J!W~qHHwK&$e
zgw+oV6WA}qV)rYYGt}Cf7jREezJ%AGp!CxqSvgV&o9!aYa9Dtgb^a7L*;5AnGQVPp
p7rT~cG}}2fuo(ImD4)T#&tVt7!I@)D)ft>3tl+8X;Z{yr{{zCLg0BDo

diff --git a/jbmc/regression/jbmc-strings/java_contains/test_contains.java b/jbmc/regression/jbmc-strings/java_contains/test_contains.java
deleted file mode 100644
index 7c0d5304cd3..00000000000
--- a/jbmc/regression/jbmc-strings/java_contains/test_contains.java
+++ /dev/null
@@ -1,9 +0,0 @@
-public class test_contains
-{
-   public static void main()
-   {
-      String s = new String("Abc");
-      String u = "bc";
-      assert(!s.contains(u));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc b/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc
deleted file mode 100644
index a61ab36b4b1..00000000000
--- a/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_delete_char_at.class
---refine-strings --string-max-length 1000 --function test_delete_char_at.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 9.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class b/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class
deleted file mode 100644
index 130e3d10f6c1fc4b451b5ce93a816a301c3171d7..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 923
zcmaJ<+int36kUhg48tH4XiKYjtqRl@snlB=BSlS&cu6oe_Jtf~PH^gU24{x;i~Rwg
z)r1<G=)3=<anH~x8jLSzpR@NqYps3x@$2h101ez#kU>epSp^Z4WSsNuc?B16(Z5|v
zB8?>(mla&WRS9JUDL=iUpo(P)*BJ6k+;xTH8Mfs<FkId<h0efs7!sR?Wq9`(qUFjf
zhFHti1w*E7SmN1muP2<Beli92xM4A*J092GKIMbJO_C(6Fvy#lc?_d;?4hHHM~45Y
z=n2>B>cSMB=xT4c)8*dkF5l-Wa>z5x`}dm3t$wZJIfm8W8XBf998%NlX)0DxlW<){
z9cwCXprIm*8HPwxBU%;fxJeunjAmHlL&vcRB>xY33Aa?-#vO+2<m2<+uF$-{Tw^`d
zA3hiei<-4kZcjdpqZ^ee*Kq+G3=6i?uW19v-WN`-^&+q#s5)**i#pOI+VyGZ5a;p#
zC}htL5ewz%L=uq@?}prT8D{^a7?-<Iq48%XHMLCI5r#QkxP~M2lV;Myy&(l?L3U{6
z(zJ^J%NG4v&@Bq)50lOUy-H*m*?9F3?4zHESvnJelOc(@lT@2lH$t(sBSc;wBKoA7
zi;WQ9uExF~v0WWOYJY-!fWmSvIfC*YsUxH)QT^`YMgrVLLMAfEWHXS+Cu5OV>QFFG
ykrdcZ)Fl)pECiuYXCn{<%;eG|oH~FM`+!*VGvo<&sM*JfBck5-D?1%fpZN{e4a}GT

diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java b/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java
deleted file mode 100644
index ffb4f48a59c..00000000000
--- a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java
+++ /dev/null
@@ -1,11 +0,0 @@
-public class test_delete_char_at
-{
-   public static void main()
-   {
-      StringBuilder s = new StringBuilder();
-      s.append("Abc");
-      org.cprover.CProverString.deleteCharAt(s, 1);
-      String str = s.toString();
-      assert(!str.equals("Ac"));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_endswith/test.desc b/jbmc/regression/jbmc-strings/java_endswith/test.desc
deleted file mode 100644
index 9aba187f286..00000000000
--- a/jbmc/regression/jbmc-strings/java_endswith/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_endswith.class
---refine-strings --string-max-length 1000 --function test_endswith.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 7.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.class b/jbmc/regression/jbmc-strings/java_endswith/test_endswith.class
deleted file mode 100644
index e3d453c444f4c7dce39962d72b8d7b7035fe7911..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 666
zcmZ`%O;6iE5Pjn~w&NHQoC2W*T1pBbNO0j+R25NrX=o2YRN+!N_KGeIPGxV}-vWPt
zGawPENc7(S)QVXb5^+FU?at1}dv9j<&%a+c05-7d!o!S>rw*REFfi+2t^gPF`tsby
z3m1-#FSvM#MH@9jr52>ANR;fw={uPQovw%obU?5+Wh~VjLax5DPcXN8ksy?sG8P~E
z#~qRE>0}NZ2Qns%wNwy(+YP>FZq`6>HpA{6hTH1(lTf^uy24i?RbNCLr9Y+mx^@)&
z2t1TfCX}_k-VNfz^_EIxe8})yoiNhjR|G>_V;J|agk?f?l)ZJ|#7>g*5?1qo!baW0
z3K|axK6Q>ns0fqw<_PCM>ucSxqXm9ufsdr{h)Scv?Jm!eFcpbZCL$W@;i;%T2Y84F
zSm3wt_@$^^)orkq1EZkK`vl+S_#{5_jRELfC&K65%AAA(D#O$^ml_<aUBhVmxdF@%
ze!h7D>lBs7>J{u06tCg52Ppj3NJfU_!(=<pGAtHgW0C*E6ZRBAfAxo$<i)P3A<afc
h4NUm%6^f^@%`=#}OIRb!dvzKo55s$_dzj8BtGCX>fW-g+

diff --git a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java b/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java
deleted file mode 100644
index 5e743a9c569..00000000000
--- a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java
+++ /dev/null
@@ -1,9 +0,0 @@
-public class test_endswith
-{
-   public static void main()
-   {
-      String s = new String("Abcd");
-      String suff = "cd";
-      assert(!s.endsWith(suff));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_equal/test.desc b/jbmc/regression/jbmc-strings/java_equal/test.desc
deleted file mode 100644
index bd4d1022d78..00000000000
--- a/jbmc/regression/jbmc-strings/java_equal/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_equal.class
---refine-strings --string-max-length 1000
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 8.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_equal/test_equal.class b/jbmc/regression/jbmc-strings/java_equal/test_equal.class
deleted file mode 100644
index e0fc6db8aaf91eb799f5e02cfdd3194a232479f1..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 725
zcmZuv(M}Ul5IwWq?rxXGEv<!$qM(Q^wDQ6mglLLB6?`Z$0Upe4dqXZPySTgc5B!P#
zfX`||6G`;lk0Q+73Jt_$b7$_HnR905?%%6lzX5EZ;ljhbjmHk2xG=Eb;AsIap6Sb?
zjU^Y3#-F=*fn^&n3FT#xBr;A_6ec?=5#2!c33N!Xwp6InZ9=YA|41-fQC|}LwhHCm
z;H)d-eVxp}nNT5NwszD$5nsf5Aj0GIP8zH5cvBZncT&+i-4*9qJ~u~jwtB%oa<>x=
z;+}l3G?kyqB>f~m4@B@<b9wMlBoy!S5{z@D!4>UA9;WfY!z<JX)k*H#o59}2aTF8W
z3A>HDhgGcI;r`G)k-d~qsr`QtD{CydmoTo{tn<eFiFPaCwenK>GEuSY-?qZLNCyn?
zP7krfPvh~!QL(BgU@r$|L6OfHzAdmNw)xc&=(|otiBBsF5(+5eA^SS@E0>yVcP?QZ
zlyW1O?aa%ww_D2Z{eU$@d985)dx)t^I0qvX{*0rI=G~}PGBTxk)?#^X(_$qXbNu@>
zS+~WJ3L`#@D>QA)j=u`SbGO}ZWNiX7CHDeTL)hjwn7N;@Cj2*(Xs$dA?~R_fn#n)9
E2H7QzvH$=8

diff --git a/jbmc/regression/jbmc-strings/java_equal/test_equal.java b/jbmc/regression/jbmc-strings/java_equal/test_equal.java
deleted file mode 100644
index e8c9ac7cb1a..00000000000
--- a/jbmc/regression/jbmc-strings/java_equal/test_equal.java
+++ /dev/null
@@ -1,9 +0,0 @@
-public class test_equal
-{
-   public static void main(String[] argv)
-   {
-      String s = new String("pi");
-      String t = new String("po");
-      assert(!s.equals(t));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_float/test.desc b/jbmc/regression/jbmc-strings/java_float/test.desc
deleted file mode 100644
index d79c25dab3a..00000000000
--- a/jbmc/regression/jbmc-strings/java_float/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-THOROUGH
-test_float.class
---refine-strings --string-max-length 1000
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 15.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_float/test_float.class b/jbmc/regression/jbmc-strings/java_float/test_float.class
deleted file mode 100644
index 00e8622e2ac6a2341fb02487fba698f9df054765..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1015
zcmZuw(Nfbu6g``!*)*iI1dFYxpn$d@R0UCKRS@WmGl)8Mbi@Y?ZD4|Ff=TKOPxu@1
z13s%W;OLC{<bxk2-c6|$agw?B?(W&U=iIyd^VjFE0H$zPLk|Y!oi~7dAk5BpK*Kql
zPhbec8b)v-ffO#P$ZIHIRK=KzOB~}Gk{INe&``u>jw=kk!)6dzerS7cuwVz~nq$=&
z*b0MEwp}~C%@E5Mo-oMsUfp6yE!nQM+-$5_{$l~Ag@$Rn41M|MOPl6vv*?)aMzI?D
zw!2Xh8<W-0ti8N%Zbf*Gs~nRIYPsed=GUrT)2~?-TVzXxRuHbPJDwR%h;%wmAj2`G
z;~J(puIspgn;bJbN+|0v&`SiD&1Fie;}(dnde2=KnYS4d<DEF$Avf1nyy*L$&!BbA
z<hY|_7IO^g4*tQ~rd126R{v3W1lUqdB0763LJ5%yz4l@zUnv}~)X_ZKL1;BdnAfDe
znHJjiiVvx%A?2~mMv3S|ryQMT;9COZP)9QP<Hv}GDAuc{=>-1(S|UpY>il2y=N-Bp
z)ZDri*uGW&Q#tBs*rWxz8!L42Qgk5!md=WXP!t0beIwgPqch|g`S|EQ*n0uQNwP{b
zNnJt~If@1J2PAOvFAQnHh%Fj&W#|*)GxD&o@eyH_4^VQ-9=P!Gp^ryi-9;g%7>PY-
zZ!wUQjjkxl<l=@NMO|Nze72A7Z-Rvsv6!YOLDYz{LLVnKD#=L@c@6#0=|LqihHgyK
z>?5S{l>92mJw>~+U<Wkd9Q~3cahz`bw4##ew*09`C(vW0_K@BMm)}8-eT3Q}(JqBZ
P8i%CMih`Y`frNqImBP|{

diff --git a/jbmc/regression/jbmc-strings/java_float/test_float.java b/jbmc/regression/jbmc-strings/java_float/test_float.java
deleted file mode 100644
index 312f1aeaf10..00000000000
--- a/jbmc/regression/jbmc-strings/java_float/test_float.java
+++ /dev/null
@@ -1,17 +0,0 @@
-public class test_float
-{
-   public static void main(/*String[] arg*/)
-   {
-      float inf = 100.0f / 0.0f;
-      float minus_inf = -100.0f / 0.0f;
-      float nan = 0.0f / 0.0f;
-      String inf_string = Float.toString(inf);
-      String mininf_string = Float.toString(minus_inf);
-      String nan_string = Float.toString(nan);
-      System.out.println(nan_string);
-      System.out.println(inf_string);
-      System.out.println(mininf_string);
-      assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity")
-             || !mininf_string.equals("-Infinity"));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_hash_code/test.desc b/jbmc/regression/jbmc-strings/java_hash_code/test.desc
deleted file mode 100644
index f863a67e57d..00000000000
--- a/jbmc/regression/jbmc-strings/java_hash_code/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_hash_code.class
---refine-strings --string-max-length 1000 --function test_hash_code.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 7.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.class b/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.class
deleted file mode 100644
index d9b3e2b2f3de9b4d49d84348b75a7e50690e3cc1..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 602
zcmY*W%TC)s6g}6EOmGYY2SR8|c_SVYY*?ZS#6v=*Wf5AbY|z9R!9Z}3?eH<I*s%sA
zkf;QE{t3h#1BuXhUiaQ}?m6S9m-`0*OPKc1g>oK)T@a{v7{V8UuO3{K1-^M0#&>}c
zLTOSaiHcL*jFNSo$XY|y3A9JZE$c|9KM3~B>|cVj)~qW+@3xNA@7768#k;1M6DLwf
zgzjo8!{cA_Gz$xi67tJo<DJ8+Hd}G1Hnl;NQkA6phcY?b51Dk~NS;X_KDr5(toiUz
zV7!kpj1wv*yV#J?!Q$$N(v3K7#)O{FJOUFwCNV`Qb}&1&BNe8fLe(_Z(E-ad3f^3?
z#Vz*Mfvq+8SqSC2N_4F1?apj6ZE=DDd#q3JBLh^d7|ndLLB<EKJ$xJHop^WW?m$<j
z5WT$SvLG?E*e?A8iw7_oSU&@6`x^E+%5%4H=6PPA@E`8KJLDb>i<PkiaQN(U%N!5>
zm&l`!BL&biMg#)>I8<u4SjyT0eSx?|{v5)&gk#^p?r?r6GdwOVf5qtU&sq+=0-5k{
AD*ylh

diff --git a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java b/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java
deleted file mode 100644
index fb01e0cb67e..00000000000
--- a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java
+++ /dev/null
@@ -1,9 +0,0 @@
-public class test_hash_code
-{
-   public static void main()
-   {
-      String s1 = "ab";
-      String s2 = "ab";
-      assert(s1.hashCode() != s2.hashCode());
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_index_of/test.desc b/jbmc/regression/jbmc-strings/java_index_of/test.desc
deleted file mode 100644
index 4cd2ce43a12..00000000000
--- a/jbmc/regression/jbmc-strings/java_index_of/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_index_of.class
---refine-strings --string-max-length 1000 --function test_index_of.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 8.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.class b/jbmc/regression/jbmc-strings/java_index_of/test_index_of.class
deleted file mode 100644
index cae397a79fb81b3543a6616e973fafdf8c8b03c6..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 631
zcmY*WOHbQC5dOxoy^b-Em=aRTD=oAEq;la_Kt<3>RZ}<wRcbECj|D9RyRseB-@=I-
zXQ%`cNc7$xg&4af5%OwxJu}~9cK$xx-UC=g(}s-+3v~-GZA{`-85X7lrfry*5SXzs
zi#dS?VQk(@Q<-Ecj?!(FdVW`i1nLmXH5I9BgHUQNekbT#aVQC+EfvX~-ia@hy}Xzc
zC!UH3!|luqj=y<7i?G0Jg0&WO|8v;wxR(U-v&s=}Cev(RMWOt)A0NCw@=iSm!x&+y
zO+O%Le!zGKZ!qs*2o9m1*Q|8C=x}B8$?m5li4)d+MkcV};4R(}Dg(%_e<XwKS*V>Q
zDmo;H!o}_ZVZ7NIApWI4EPmmJ2hpuAzZIbt%2XvX>^tGkvmPh-p*m>rQ`<ZRs?>Au
zd@F%nVubfm{+s5L_%xPoK$m$TD!iLTkWfaoU)q7jU|`PGzPhE>((*O*^(z=>s7&eS
z7`lV`;|AhS&Y~48H5hz17-jM&Sl;4Em*H~M0X<+=V2l^f1~2+LtA#dDb**cZ&mi;*
Y=%wE<2E<SHav}qo^D%E?ywI&Z0#{ph8UO$Q

diff --git a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java b/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java
deleted file mode 100644
index 96763d04847..00000000000
--- a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java
+++ /dev/null
@@ -1,10 +0,0 @@
-public class test_index_of
-{
-   public static void main()
-   {
-      String s = "Abc";
-      String bc = "bc";
-      int i = s.indexOf(bc);
-      assert(i != 1);
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test.desc b/jbmc/regression/jbmc-strings/java_index_of_char/test.desc
deleted file mode 100644
index e91db762b07..00000000000
--- a/jbmc/regression/jbmc-strings/java_index_of_char/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_index_of_char.class
---refine-strings --string-max-length 1000 --function test_index_of_char.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 8.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.class b/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.class
deleted file mode 100644
index bf4fa6e946eca6e5f9872d09a06a2f839b17d288..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 614
zcmZWmO;6iE5Pg%_*<egD0Yb`011&|s0WKU<1foSk{os(Q0xr?UUg$!w(b_@$7Eata
zLnV+vYVZ9~sIyi{R8=eO$IQI<=FR?odiV)o4GSIyP%UG^Lk%wnATTK~<-tW&VA{hB
zUJ29*qw_LNmC1Axr|)$t+Z`1V=zvga=vZg#gyQ1TH-fX3M2ax{Nyq9-_q46dS6j@9
zQ>kOZP&1R^$!B?%hXrN{<wn@~%i%SXt_jt)wup&LrCCeIk-BIlhpq6tG%LsQT>9`a
z#Cn_Uknuj|@Y;umK|;-@S35F3THSnZ_k%HsAyob+6L{le9&ZUjAGg~+R$=x}sF@iZ
z9}z^}%I+b1S=?FLVUvB>R)^<9s75N)Mnye!cAIrM!NWP=Mg>nBprB^^<y#SC&G7z$
zUo(6XpYHNK=*AXenD<g1B!&jP(mfOy49r#vAA_*5JavcSyIVMy2&UaD3_il$zenkp
zWhvw=RsK_^W>krnVA(S2%sIkQ5A=k(K!x}>FxpdD%awtVinv4h62iHLQ~Uv^Py5`Q
PrEyX4H>`!RTy^{pE-iAY

diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java b/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java
deleted file mode 100644
index 999b50f6896..00000000000
--- a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java
+++ /dev/null
@@ -1,10 +0,0 @@
-public class test_index_of_char
-{
-   public static void main()
-   {
-      String s = "Abc";
-      char c = 'c';
-      int i = s.indexOf(c);
-      assert(i != 2);
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc b/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc
deleted file mode 100644
index 0fd3fc08bb0..00000000000
--- a/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-test_insert_char_array.class
---refine-strings --string-max-length 1000 --function test_insert_char_array.main
-^EXIT=10$
-^SIGNAL=0$
-assertion.* line 26.* SUCCESS$
-assertion.* line 28.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class b/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class
deleted file mode 100644
index c19a742c0f4ddb43f1234627a0ee00cf490fecfb..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1416
zcmZuwSx*yD6#njXxn-Er(w2&V3JBVTQWso{3zS8aO%aG&$g~}Cv~=ps)WmoHggpA<
zt71}&8h!WA_--P4?zFXml1c7z=A7?*=R4>A-23t!z!+9!L=fYM`;d?!At{y-v7}^#
zFe)RBGd`RZmve16k1-h+aIuZ9mwdP^;|i{FWMl*d%D9YcxXy8dAv~m7mS)<zQL?6V
zOU)Iv0t0)<;2qaXx_zC&6^pMixU)t<V+hRaC2g^?mD9}o!kMAdvQ53Tx%4#qOf@G=
zQ+>@4jXlc7=bx*u)O1lTZKhWomkfh{#a8n#7Sys6O!ZJ6y(9=QoQSnVOjh(_K{GRR
z1SdFbsd|aF*j#*#<0i)hgKs=vtP_=2jEb4pW^_TT*VZh1qlUeaCu$q2;5I5qDL8^|
zh9d_F*3&UScuXqDVoJd@W)$?Ik7HKB3EX0k)PgwmbId8YjXNCk3Km2_7ox;Z&E*S3
zPQfCU7`mHjCK_5#o2FrsPKT4^SXOWs_ZWiB*rnWaEl)B@kFxvhHEkKXTII_K(Y$K8
ztd*##eX&D&(omR$w2cN-Bz9=?jvD4>I$t)8SDKm5E<1Z8WVSVX1A4Bdt(jK%hV%Z?
zUR$=dMH6ULsPL{Dj&7uvY2a+itf^ZxQ(;G={bmMU7EVPP7q9lRq86<K3f1Jy#A(t4
zO_8%jdJfc=f@bNaR`}m98e6+UKj<wy!~ngj2t7*{>=q5DlLs_S=%)23-Hy>tGXzg!
z7wn^OL=UZA$H>qohKbI?bptN?fZ?x@9)w)GaL>E0^(DT)LuWG4H&%sb{f)%l|NWJ$
z!ux?7B?l@>83mvWPF#Fs<LD>gV`Nnz{ei-9oc%_aY&56!WGPDJCJ+C}XYj>DZ|XCA
z>rH+g4ii5?cMwQ`LI*Hd58bJUK5=-q37(#Bo`n%tFt<A54(3;rZUU7B%f%hEr>anT
zw$ZZ#|2C4TP)8MkZ47=z@WC!Re>mny&HNVa4YQz9t8WzTbPiE{VImWuwTsk^;y9^%
zl1>Q{Z<MN@CLteF)uQeIq&-Yi-5e)5hN2|P@c)*KIoboAp->g!ZE*K{xLu#%Z{}>Y
RM__p%DK|wEPdSuM{{uprGQa=;

diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java b/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java
deleted file mode 100644
index f392655afc1..00000000000
--- a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java
+++ /dev/null
@@ -1,30 +0,0 @@
-public class test_insert_char_array
-{
-    // These are models of the String methods manipulating char arrays
-    public static String stringOfCharArray(char arr[])
-    {
-        StringBuilder sb=new StringBuilder("");
-        for(int i=0; i<arr.length; i++)
-            sb.append(arr[i]);
-        return sb.toString();
-    }
-    public static void insert(StringBuilder sb, int pos, char arr[])
-    {
-        String s=stringOfCharArray(arr);
-        org.cprover.CProverString.insert(sb, pos, s);
-    }
-    public static void main(int i)
-    {
-        StringBuilder sb = new StringBuilder("ad");
-        char[] array = new char[2];
-        array[0] = 'b';
-        array[1] = 'c';
-        insert(sb, 1, array);
-        String s = sb.toString();
-        System.out.println(s);
-        if(i==0)
-            assert(s.equals("abcd"));
-        else
-            assert(!s.equals("abcd"));
-    }
-}
diff --git a/jbmc/regression/jbmc-strings/java_insert_multiple/test.desc b/jbmc/regression/jbmc-strings/java_insert_multiple/test.desc
deleted file mode 100644
index c1a8a213da4..00000000000
--- a/jbmc/regression/jbmc-strings/java_insert_multiple/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_insert_multiple.class
---refine-strings --string-max-length 1000 --function test_insert_multiple.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 9.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class b/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class
deleted file mode 100644
index 9e6a87de460edd04e3d7b1da2ef15b32d1eece00..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 979
zcmaJ<ZEw<06n<`Dw3Kcz#x|JFIh_hjhcC!f&`j|qMtn&yF58!-v^S))wAhyY7xxGJ
ztR}FyM8Er=G@c6sqL_WT=k}cQJm)#L&(GiAz5^)YzKR6S$yiZvUWJ5J6&G+(!J3Gd
zMCNi7Gq|E4t0ITIjCB>7KwMRE4I45F40CI`?{hD(T*rTG`Fg|VCIj1Lh*T`c3LY?o
zvblE*;i_wLhIq|#_^VE<!M(SlnF=l4au}xTfo{Biski%SQYGU$gHkc<6B@Pdc07YW
zwFD>=a6j0y95H&Y)v*JsZS#$N{Xo|+hZMu2xEE~QX%^~%XF1JB9m_Vk#~|sZ=(!=|
zriNQ6lG=v2+}2RSriNK0NtE6&Oj4lX4(>9f$7~OW>pt;3m*`UeQzGM@hB7J)i81nZ
zW1kzrU#WpKhWTu5+&4&;#iM0huURnKo_oN(LiJ5Q4l$9z_6(&-@X4~}=hfT<@vz45
z>=fVxtb7`i61YQIsqAE9ncToXbadPQXVt-zlyhX4`1k>;HhGF+!Q{T>adY(I<dC34
z1v1nwR>_(P@-a)K#V?~<2xLd3=$xmoWr~dARK5rHSu|pS&PYGW5XIuCH6W-&wasHl
zJIPQF;TQRE!Z^azc0Qbp96{dBccIk2AbN<@dQ$Bo_7SmTXgfVj{}AL-pL~hvX(CjL
zNyu1&f)yH7qD-19F|c1K$;b>!XGRK&eO170a;A&;A>{BUghO8u9di$b3!W)R+Ll=F
IY=89fA9A7H#sB~S

diff --git a/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java b/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java
deleted file mode 100644
index e9ed16a8e91..00000000000
--- a/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java
+++ /dev/null
@@ -1,11 +0,0 @@
-public class test_insert_multiple
-{
-   public static void main()
-   {
-      StringBuilder sb = new StringBuilder("ad");
-      org.cprover.CProverString.insert(sb, 1, 'c');
-      org.cprover.CProverString.insert(sb, 1, "b");
-      String s = sb.toString();
-      assert(!s.equals("abcd"));
-   }
-}
diff --git a/jbmc/regression/jbmc-strings/java_insert_string/test.desc b/jbmc/regression/jbmc-strings/java_insert_string/test.desc
deleted file mode 100644
index 698c2b13e34..00000000000
--- a/jbmc/regression/jbmc-strings/java_insert_string/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_insert_string.class
---refine-strings --string-max-length 1000 --function test_insert_string.main
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion\.1\].* line 8.* FAILURE$
---
diff --git a/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.class b/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.class
deleted file mode 100644
index e5990e07a15d25e478bdb5a83afa107b1553147c..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 897
zcmZuv*>2N76g`v8j^mKjNs|;PP$-b35VM3e6#~K{L|CLCQ2SCj_9(cxcCnrQ3;h9}
z0VzRLf_MH2#2u$e1mR`o&bjBFyUhLh``dQ_P25(H!?J`EGEORp;gpOO1*dUFJXX`l
z;;f8w3eKY{p{5`s$aMv4xFF#oLt)hj0`7;l=LQe#!00*LVqlvLsdd}6!#fP|YV9>c
zqU~9nA=j~8{(P|0<Nhl_CdZCpyA0WGXqfMw8M_fo1xaWy$m^zaD5G?}fp79hwg@VR
zJP5aJSESwwLf>}#jcsGkP@$nfZei<=;r8`z<h(zy9gF)6F~brZovfZI;gX8WxT4}J
znkw>GpmL0!X;E$!*KnPoGE=%YY4oA*dnBdJ*C64BikrB_ke|i9=xuW|{0kZv#jsfI
z%y?t4C5E-+`F-8o^}Rjr>+P4(J&8$;yJmPiAAHzm>&bs)=b#ChrW|?`^<uR)M{Ln&
z^7jM73I3^g+*zweznz=)(ROGh7)lloY@b`xvC#*I19H$lY+{8rD@Pm1@)a?6vf`kT
zqCjVnUdwbdx|8)0*e5~6BAuxSWJselrM{)m82R)A#5T0}2#KflgqHk@)SLPcQs*<|
zeH7QU^bpDiWDbzo7(x9ZL}QU?2}!b(P)J^bgfe6_C`Fmj4A?I;Bvd3U5qxx-wHZ|c
iENIywj_gB9d_*Gt1@cUHQmoKPBBtIIEgg%}9{&TDpT%JS

diff --git a/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java b/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java
deleted file mode 100644
index ad4d0894665..00000000000
--- a/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java
+++ /dev/null
@@ -1,10 +0,0 @@
-public class test_insert_string
-{
-   public static void main()
-   {
-      StringBuilder sb = new StringBuilder("ad");
-      org.cprover.CProverString.insert(sb, 1, "bc");
-      String s = sb.toString();
-      assert(!s.equals("abcd"));
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_append_object/test.desc b/jbmc/regression/strings-smoke-tests/java_append_object/test.desc
deleted file mode 100644
index c905a3990f6..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_append_object/test.desc
+++ /dev/null
@@ -1,10 +0,0 @@
-FUTURE
-test_append_object.class
---refine-strings --verbosity 10 --string-max-length 1000
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
---
-Issue: diffblue/test-gen#82
diff --git a/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.class b/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.class
deleted file mode 100644
index ed6942a1fa6ddb20c36b528444d598e867e347f5..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 992
zcmZWn*>2N76g`t|9M@^mbPIb6p(Jh7u#`2SEAT>Ekb*$;rE=nF<>J`E3ld+!dwzgt
zij+!Jf_FX&xZ{wfX=VG4=gygP&s~21`SBCLGB#C=VMf8Mg6kYNRKzeNO<tOtNzCDv
ziUNvBq%p5xLB%3U97`%vnBgd^xQ#m;cNxa>y5|YkHyzu1W_o(V5(Wd?VMtU>+w@l$
zqJ`pHhS;WK2!?dcw8eJNY6$m@1k*uFH*JPg-PfBRw)A%BCT`NjagRZ%Hm(0mYTXIk
zrg&k>d(*z~{9V1>7PhhLG!8`5Upmk~=^7?5NwkK!w?|9E3M5#blr7!fFV}t7wD&gx
z(=vpsQ8Dgocz}l-k2E~S6OM|8DxPY{Vw|E&8p%OgG^}8iAvfS!@8|y9bsd)>dtMXA
znuc|3Fk}YzUWIapTs>J-wq8aIr9$oOg-Y?1YbcKjDfOK`$3)>gkPxQ?)IWQ^Xi;yR
zz-O53(V9;AHPyx^8lku7!gwfP*v-J(5@b=&CQnQ31+U0nC&b4<x4bieUec8!%|?2V
z*``GU#4u$D&vb=xQc)TQKcEAeo*m569FEcCvP@34h5n*ovd?6vXm^EHMr(Zj2<)2#
zVw!9sbTTB7JAr;dgk~J5W+N}N(b_R$?~f4QTAc49u|VIu#V+{vA(T=V$wR0eOq8-C
zU1%MQ93w^G(O)t`B#bae+!U7NB<N8v3YBDyP`nh08bzLjSCGL4LXp_Nw25(C4Btx}
sm&vUVu%E|rC>R*arn|^=z++z#i++bXh}h3bGR6_n)@0^aX%oS<e{GZ1nE(I)

diff --git a/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.java b/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.java
deleted file mode 100644
index 121690451ca..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.java
+++ /dev/null
@@ -1,17 +0,0 @@
-public class test_append_object
-{
-   public static void main(/*String[] args*/)
-   {
-      Object diff = "diff";
-      Object blue = "blue";
-
-      StringBuilder buffer = new StringBuilder();
-
-      buffer.append(diff)
-            .append(blue);
-
-      String tmp=buffer.toString();
-      System.out.println(tmp);
-      assert tmp.equals("diffblue");
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_char_array_init/test.desc b/jbmc/regression/strings-smoke-tests/java_char_array_init/test.desc
deleted file mode 100644
index c5e050b4850..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_char_array_init/test.desc
+++ /dev/null
@@ -1,10 +0,0 @@
-FUTURE
-test_init.class
---refine-strings --verbosity 10 --string-max-length 1000
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
---
-cbmc/test-gen#259
diff --git a/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.class b/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.class
deleted file mode 100644
index 48075eb9187d595911a17ba978135e4608218804..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1046
zcmZuw-%ry}6#nkk?rx>9GGO8l5EOL`WQzE66TtyO1T~q{01u{YH(2aiY&)ZWg+BA*
zqt9ZpC1Uj5KgdVoxt)xWm^SB}d(U^y{m$3h--q9S0+_)g4JnLpjB1GBf;1Ns7{etQ
zUDj{~nFI`sb7VCnFd}y*;+T}_t8q+8pX0cu;X0-{ZZPzXnZ7T)z;Ydb!Sc;5TT~g?
z21Bf1IaV;s5Y3FgU{H!~RWKx1Ek``5*S3WBT!JZ4GcAXqyA+s}H*4l@xXm#`BpKp`
ziv6#RR&wiJMJ!pes3#D9@JeQ;cFcFCjsc_@3>oKa)7j3I0?%@`<^D}+ZgJe!aR+yG
z+(VwDpyNJfb@ZX1Veq(Y{%Dv*&vQKqdcY77wvIW>GpNhLwp|?$QDjK8IdClKSj5r^
z22ZzkL?xi=O~R^~&7xF+lV4epQ76|AejsWjlv^kKz-maxa&ymUgn$MSW-U*8+QQim
zUWa<FknsOOQU6_8W0RgrCOl>!(`wftN?slx6L0IL?bC6cfEMTcIDJ0N4@@ucUt03W
z6QGu~At-sQT+ybBz>uyA-||GYEhK%`piT+81sfQp%ax*w$c#ZLJw;JaccjUlqSX+2
zMqbS}!M;i$2Fb?4O;Q}E+t5EysTlZVXg}1)*{HEx&MJl|XH~;4XJgWE!z~{mvQEvS
zt6`w1O(<*oP$wFQHNf`~-$TD#7}{ra9U!sZg!Zci=pr}S067VoOz91D?{$L0+Eh;i
z$&PKwIuf#;MUrBbo)|Q6TE%H(IfI5_bkVP+V;VguP^Lt}Y@in=$@8A1`AEn!RBa%7
zh!V$Hj&t;mrK!hITZ5TU7oay~G|;;Tu6%(K{f784i6iM`GZhhiP6|96ay<VRouJTT

diff --git a/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.java b/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.java
deleted file mode 100644
index 8e0f656e3e8..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.java
+++ /dev/null
@@ -1,21 +0,0 @@
-public class test_init {
-
-  public static void main(/*String[] argv*/)
-  {
-     char [] str = new char[10];
-     str[0] = 'H';
-     str[1] = 'e';
-     str[2] = 'l';
-     str[3] = 'l';
-     str[4] = 'o';
-     String s = new String(str);
-     String t = new String(str,1,2);
-
-     System.out.println(s.length());
-     assert(s.length() == 10);
-     System.out.println(s);
-     System.out.println(t);
-     assert(t.equals("el"));
-     assert(s.startsWith("Hello"));
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_compare/test.desc b/jbmc/regression/strings-smoke-tests/java_compare/test.desc
deleted file mode 100644
index 8f967c8dffb..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_compare/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-test_compare.class
---refine-strings --verbosity 10 --string-max-length 1000
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.class b/jbmc/regression/strings-smoke-tests/java_compare/test_compare.class
deleted file mode 100644
index 3a807f4d203aecb2c12a4dab57637aeb3ded9359..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 623
zcmY*WO;6iE5Pjn~w&NH`%vTBxA1!SINaex}RJEcYA=37c2njCL##y1IiH+7ye+(Cn
zoM|PHiqziuPgI?CA!)U%+1)oYZ{Ez_{r>S2z$O|#e9U^Nd3aKShdCefc<Q3=!@;bJ
z1s{u8a<NR9ToGw1b*7RyeXml{>B%mEjtS1TidFW8P-v_k66~F%D+v=#70Zu<en;xI
z31&xMsF*O;%0%?#gE-4!7taXZcGP>|@LS11M{-Y@jA|y+>~oa#&xDq*PsLXeU<~5~
zOLUCkXBh!g1bB`WLd}G1^hA8J@$OOVuGWbr1piXGcoE<wUJ)vzj8C0Y8D;-LtxT)<
zgiv~r&`t=`jpiulZ@|{-KKDC9cX~W3!c14DO3Ut03OAk&*uir;#xjrF=TD$Y%{0Nc
z0(dwWXFI{KI-kU6aqR|lWdc!Q>*OFyLUkD0g2fA12(5##(EJAb98+uS*C^T-DBr?4
zx`F%4a9BA<2%GOkF6i*$-)1QxBW2J%>MkaEGc+|Uu$dPHs-bs{(m7oF5_aJ`>=Eaq
RF2hrV6}&a-r}L6Ce*kI)bz}el

diff --git a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java b/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java
deleted file mode 100644
index c052ed429bd..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java
+++ /dev/null
@@ -1,9 +0,0 @@
-public class test_compare
-{
-   public static void main(/*String[] argv*/)
-   {
-      String s1 = "ab";
-      String s2 = "aa";
-      assert(s1.compareTo(s2) == 1);
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test.desc b/jbmc/regression/strings-smoke-tests/java_concat/test.desc
deleted file mode 100644
index 2672b7502d2..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_concat/test.desc
+++ /dev/null
@@ -1,9 +0,0 @@
-CORE
-test_concat.class
---refine-strings --verbosity 10 --string-max-length 1000
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion.1\].* line 10.* SUCCESS$
-^\[.*assertion.2\].* line 11.* FAILURE$
---
-non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.class b/jbmc/regression/strings-smoke-tests/java_concat/test_concat.class
deleted file mode 100644
index 8802b3957d256ad0dd0290b78212e49734f7f807..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 847
zcmZuvT~8B16g|`KSGNn4VzCtwL9A^B>PPj3#z?9pL_kc93A~u?c2XA0?q+t&kKsk%
zd{&dzNTTolDD}=_TZ}x++_~r8x%Zqq^YhoY?*M9eWMUF?I<6a-H<7>%xh)vDDea<(
zCEQBE!m^IrCQO-GG;s$d9c6}@WjhSHh+N+bpShvk>hd-NJ7Cc2uIENi7?P#(8wRD}
zw>iVqw(IfT-f@eI*D{#`$F}P+Of)0gdADN+F-&Y2jJnhPTf=PnJ>l?8SKi1(JdEBt
zzUSD{+L3)?TbM?caCxqFZLd>pM#A+v42i&%!HR{uSRpDw;9FS5nvSZ4d$@053K@p{
z_~yn?&T}Dr!H~YtOveKY4^jK4)yviqcOr&dX?tAdy#Klsu64QBi4NmAY>|7;o1u7F
z{{JNy3cl!6oj~{}TvQu-u^sBuoI_h|Q1{tOs%@1UH1IL0Mwi}-QrkRq1#gd((&VEa
z1?Zs;ut-lmN&kXn@^UtGN`lGx(mq4pJXuCotqj0E$wXYCU5i166mp}~4|G+f*sC)n
z_Or<Wloypg)Oze{<nB~f`p|b*=f1*ttb9i56xp1T3Em@p26KOa^p6qfUjSv>MBH`>
z2Ax&<mKw3uQ6PVTNE8WKM;d#iW|lH?Nc<*1)p3>4k_J@3Kz_uw7ApXzvsNDyr_hy;
YP?BGe8h0CtloeGZtfz7mg_z8>KR*en>i_@%

diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java b/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java
deleted file mode 100644
index 9e861e722bf..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java
+++ /dev/null
@@ -1,13 +0,0 @@
-public class test_concat
-{
-   public static void main(/*String[] argv*/)
-   {
-      String s = new String("pi");
-      int i = s.length();
-      String t = new String("ppo");
-      String u = s.concat(t);
-      char c = org.cprover.CProverString.charAt(u, i);
-      assert(c == 'p');
-      assert(c == 'o');
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test.desc b/jbmc/regression/strings-smoke-tests/java_delete/test.desc
deleted file mode 100644
index 7fb479f198b..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_delete/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-test_delete.class
---refine-strings --verbosity 10 --string-max-length 1000
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.class b/jbmc/regression/strings-smoke-tests/java_delete/test_delete.class
deleted file mode 100644
index 44a8fdc10db2d6d2f74b2300b796753d55a27517..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 856
zcmZWnZEw<06n<`@6iPQ3V~nX&r&EDB@CBy{ixH<Li};dYG}{+b+8ff@wez;@$M6UI
ztR`SwqTl^b8qX~QbbRSOJ?A;kdCtqPKi_`<sN;c-d0f!2n#4sN3NGomj5TRpNx{I?
zB-V9Y!*vZebm$UU(osf5!v@3Rx)}sqgpTh8Pn^K)xZGx7`wWR~$8*Am46#!AEkk_A
zw>d+m<#_yM@36zg8wsYsq3L)GbM4TyKD;oGA~&hgaFZdqZMmm3dfV>_i$8N@Qa0p4
z_}=C&4|(;#JT?t1AjhyQ?V4+P-C8>oj@NzMb6lGXQqk;K611tIYM_Q&25#eyfef+?
zO4Fip2JWKHP@Hl!$Gtrj!Y7jSKV>!CGq8pGBxaiMs&l}t@ITi`2g6dSHN}mb4LO(<
zUvz8Mk?@bXsO`Lt-f>Q1)FH#xZ1QPmjosby4DmQd0}TB!S-vz2Y|x(g$DZj1X9SKK
zX_RS^nW^j@m$uDNuzBDJZcoNTy9;|1pjGc<jgDrXE{kQ0a=K*2z~p-9yGVbl^fG$Y
z$`I_c1R_u0MC4>hVQB*GQmR6+>Isy+Tx^K=^GaO(2K8NKfJEyHv_A41x#R$;KGG-9
z_l8LSl$=V$S%6BmN>`g80U8QOVv{Nq$eRZHEw5o&Ly_DolcM!V2(XYd2AJzZi+@5q
X_7&QccdS+Ns8EbYvZHfR+4Fw^Cq%Z1

diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java b/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java
deleted file mode 100644
index 99298e536c3..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java
+++ /dev/null
@@ -1,10 +0,0 @@
-public class test_delete
-{
-   public static void main(/*String[] argv*/)
-   {
-      StringBuilder s = new StringBuilder("Abc");
-      org.cprover.CProverString.delete(s,1,2);
-      String str = s.toString();
-      assert(str.equals("Ac"));
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_empty/test.desc b/jbmc/regression/strings-smoke-tests/java_empty/test.desc
deleted file mode 100644
index c1dae21b4d5..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_empty/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-test_empty.class
---refine-strings --verbosity 10 --string-max-length 1000
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_empty/test_empty.class b/jbmc/regression/strings-smoke-tests/java_empty/test_empty.class
deleted file mode 100644
index 8e9a17d387e018eab40fb786dd1c200c507739da..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 571
zcmY*V%T5A85Ugf_!F3fx#YM%piF%L=M`JX;4!#Z;6TO%PCT0{CvpbmhEBt_GHGxDE
zz57kZ*t1cHm!5u9RaejF_v<@=5|(WYAeX|#00dkcc}xmS*+?KKFm0oN8G%{C=#m$P
zGSI5&hr25DDs@>S&?O<cp?sw`3D(N$IU&B&tVu%pNcr-l)u_ne%z$~&@RUy&Dr>KL
zd+gmsZGkyLYNJ~J)v(LWR#27u$}rMehWbi2?)1a@jd$-ka4<yRXk(C>4(72yaLue(
z_x$VP_MgYSAZP{zyRRUy=wQj<GkyGN<wjQZzgAfX%D*NE74DhM(OrCIy3g9F^Is5h
zH5sZv)_P0%GTjQ<l;A%FDB~KVoLL}ao#QZ91%CMoB-Xm1Cj&&9V=`(IQ!_p20b)@%
zpN$<p!)hbD)<L|D!8ar>x=4N)dMu(3^A^_Rn1ss?Mz~6WzTgUEIUDVXmLf@DBr7^d
cwISk<h+8kP`eJ`xj7S18XUjMqi*}9w0K8&p1^@s6

diff --git a/jbmc/regression/strings-smoke-tests/java_empty/test_empty.java b/jbmc/regression/strings-smoke-tests/java_empty/test_empty.java
deleted file mode 100644
index 47c335e16fa..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_empty/test_empty.java
+++ /dev/null
@@ -1,8 +0,0 @@
-public class test_empty
-{
-   public static void main(/*String[] argv*/)
-   {
-      String empty = "";
-      assert(empty.isEmpty());
-   }
-}
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_int/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_int/test.desc
deleted file mode 100644
index 66c81170630..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_insert_int/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-FUTURE
-test_insert_int.class
---refine-strings --verbosity 10  --string-max-length 1000
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.class b/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.class
deleted file mode 100644
index 2ba5491c536729b6a634bedeb50a64d089b0e24a..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 866
zcmZWnU2hUm5IuMKSXj1&Qc9^>wOSRn%4)@GLSs~_Nh5wF7)|?PF3SyW-R{=ir9Xy0
z;Io>5v5CI>pES;03dHiVGdpwU%$b?{`|ppR0BU%kVICJ$tfp{LgMv#ME@Mr4SJKdN
zHHCEz*Kl3M4Go$^mNishsMugwT<1X`{LuE?V8;%4+YucGw$G5<wp}}X$Pg=6-ZI1+
zUPmxwo3<-n_72;^e<Q(^IOMj=FxLvX_3;Hiio&Eu#Z89Pw&k4CXf3bjTjH55iwdC#
z!uPf-TayW^2mF}pSU{d(S^B2K-LBaRecSCm>Df+4_zViSB<7Zistyykb=<+Gjx2H{
zgV#1K>Z#){Y7C_*$>Z^WPkrAbmh73{D(>mn!hMF^wCGj)Kv>~_p^+GdrE+tM8wKlf
zLo1%&HLWAxI~Km#cpcesO>#6U!`5u^>3H?s-O3E{I7gcdy)jv#JPWMT!NjK?cY-ql
zM}yQWbkXcocEh2wGZZ@_uzk^)tcZ>n_9#I&-^Uugo_Ts=ELV~{CNBmiZ$#fk`dcN-
z$R>;-*cS;zfxgKo$dJa;1p0wW70Q_>Q1<e%A>z-Cc+U8a#5-evWb-T3J_;N8)Bx!|
zGAGdXhRFPqq)J3uM1uSTz278}s#rz}RccYBXa?*LsuWXEqVUS3Yb{a&Eade8=K4_M
ZpAnCJgF59Mi<LYHDEcEg(z&SZ`F~buy2}6n

diff --git a/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.java b/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.java
deleted file mode 100644
index e480683821f..00000000000
--- a/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.java
+++ /dev/null
@@ -1,10 +0,0 @@
-public class test_insert_int
-{
-   public static void main(/*String[] argv*/)
-   {
-      StringBuilder sb = new StringBuilder("ac");
-      org.cprover.CProverString.insert(sb, 1, 42);
-      String s = sb.toString();
-      assert(s.equals("a42c"));
-   }
-}