Merge pull request diffblue#1410 from LAJW/fix-test-gen

TG-634 (Rollback) Remove invariant causing failure in unit test generation involving CharSequences
smowton · Sep 20, 2017 · b4f57ee · b4f57ee
2 parents 93149be + bcfb914
commit b4f57ee
Showing 1 changed file with 0 additions and 7 deletions.
diff --git 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");
-        }
       }
     }
   }