From bcfb91493d388d974cff46e00dda6fe6a8e74589 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Wed, 20 Sep 2017 17:03:17 +0100
Subject: [PATCH] Remove invariant causing failure in unit test generation
 involving CharSequences

---
 src/java_bytecode/java_object_factory.cpp | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index ff2ae2784eb..9324093dc82 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -882,13 +882,6 @@ void java_object_factoryt::gen_nondet_struct_init(
               binary_relation_exprt(me, ID_le, max_length)));
           }
         }
-        else
-        {
-          INVARIANT(
-            class_identifier!="java.lang.CharSequence" &&
-              class_identifier!="java.lang.AbstractStringBuilder",
-            "Trying to initialize abstract class");
-        }
       }
     }
   }