diff --git a/jbmc/regression/jbmc-concurrency/CMakeLists.txt b/jbmc/regression/jbmc-concurrency/CMakeLists.txt
index afe0ea5761a..25982e8508f 100644
--- a/jbmc/regression/jbmc-concurrency/CMakeLists.txt
+++ b/jbmc/regression/jbmc-concurrency/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc>"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
diff --git a/jbmc/regression/jbmc-concurrency/Makefile b/jbmc/regression/jbmc-concurrency/Makefile
index ad6e5381fff..e330a0eea3e 100644
--- a/jbmc/regression/jbmc-concurrency/Makefile
+++ b/jbmc/regression/jbmc-concurrency/Makefile
@@ -3,10 +3,10 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc-generics/CMakeLists.txt b/jbmc/regression/jbmc-generics/CMakeLists.txt
index 1c5fc08cf6b..507772ba3e0 100644
--- a/jbmc/regression/jbmc-generics/CMakeLists.txt
+++ b/jbmc/regression/jbmc-generics/CMakeLists.txt
@@ -1,10 +1,10 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc>"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
 add_test_pl_profile(
     "jbmc-generics-symex-driven-lazy-loading"
-    "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
     "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
     "CORE"
 )
diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile
index 1639d08dea4..592bd2d0d96 100644
--- a/jbmc/regression/jbmc-generics/Makefile
+++ b/jbmc/regression/jbmc-generics/Makefile
@@ -3,12 +3,12 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc-inheritance/CMakeLists.txt b/jbmc/regression/jbmc-inheritance/CMakeLists.txt
index afe0ea5761a..25982e8508f 100644
--- a/jbmc/regression/jbmc-inheritance/CMakeLists.txt
+++ b/jbmc/regression/jbmc-inheritance/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc>"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
diff --git a/jbmc/regression/jbmc-inheritance/Makefile b/jbmc/regression/jbmc-inheritance/Makefile
index ad6e5381fff..e330a0eea3e 100644
--- a/jbmc/regression/jbmc-inheritance/Makefile
+++ b/jbmc/regression/jbmc-inheritance/Makefile
@@ -3,10 +3,10 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc-strings/CMakeLists.txt b/jbmc/regression/jbmc-strings/CMakeLists.txt
index 1b698f38161..c7b8343e59c 100644
--- a/jbmc/regression/jbmc-strings/CMakeLists.txt
+++ b/jbmc/regression/jbmc-strings/CMakeLists.txt
@@ -1,10 +1,10 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc>"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
 add_test_pl_profile(
     "jbmc-strings-symex-driven-lazy-loading"
-    "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
     "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
     "CORE"
 )
diff --git a/jbmc/regression/jbmc-strings/Makefile b/jbmc/regression/jbmc-strings/Makefile
index 6a87a176e59..1cb0d87fafb 100644
--- a/jbmc/regression/jbmc-strings/Makefile
+++ b/jbmc/regression/jbmc-strings/Makefile
@@ -3,20 +3,20 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc/CMakeLists.txt b/jbmc/regression/jbmc/CMakeLists.txt
index fa345944621..561fe5ab0c7 100644
--- a/jbmc/regression/jbmc/CMakeLists.txt
+++ b/jbmc/regression/jbmc/CMakeLists.txt
@@ -1,10 +1,10 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc>"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
 add_test_pl_profile(
     "jbmc-symex-driven-lazy-loading"
-    "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
     "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
     "CORE"
 )
diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile
index 1639d08dea4..592bd2d0d96 100644
--- a/jbmc/regression/jbmc/Makefile
+++ b/jbmc/regression/jbmc/Makefile
@@ -3,12 +3,12 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/strings-smoke-tests/CMakeLists.txt b/jbmc/regression/strings-smoke-tests/CMakeLists.txt
index 0b63a67939c..e3584329528 100644
--- a/jbmc/regression/strings-smoke-tests/CMakeLists.txt
+++ b/jbmc/regression/strings-smoke-tests/CMakeLists.txt
@@ -1,10 +1,10 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc>"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
 add_test_pl_profile(
     "strings-smoke-tests-symex-driven-lazy-loading"
-    "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
     "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
     "CORE"
 )
diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile
index 6a87a176e59..1cb0d87fafb 100644
--- a/jbmc/regression/strings-smoke-tests/Makefile
+++ b/jbmc/regression/strings-smoke-tests/Makefile
@@ -3,20 +3,20 @@ default: tests.log
 include ../../src/config.inc
 
 test:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
-	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index a17e8ab6033..96bda1db533 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
@@ -170,7 +170,8 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
       symbol_table);
     const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
     code_assignt get_argument(
-      init_symbol_expression, symbol_exprt(this_argument.get_identifier()));
+      init_symbol_expression,
+      symbol_exprt(this_argument.get_identifier(), this_type));
     get_argument.add_source_location() = synthesized_source_location;
     new_instructions.add(get_argument);
     create_method_stub_at(
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 8ea70017c47..f946da31a50 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -369,6 +369,16 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
       "symex-coverage-report",
       cmdline.get_value("symex-coverage-report"));
 
+  if(cmdline.isset("validate-ssa-equation"))
+  {
+    options.set_option("validate-ssa-equation", true);
+  }
+
+  if(cmdline.isset("validate-goto-model"))
+  {
+    options.set_option("validate-goto-model", true);
+  }
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 
   if(cmdline.isset("no-lazy-methods"))
@@ -553,6 +563,11 @@ int jbmc_parse_optionst::doit()
     if(set_properties(goto_model))
       return 7; // should contemplate EX_USAGE from sysexits.h
 
+    if(cmdline.isset("validate-goto-model"))
+    {
+      goto_model.validate(validation_modet::INVARIANT);
+    }
+
     // The `configure_bmc` callback passed will enable enum-unwind-static if
     // applicable.
     return bmct::do_language_agnostic_bmc(
@@ -585,6 +600,11 @@ int jbmc_parse_optionst::doit()
     // particular function:
     add_failed_symbols(lazy_goto_model.symbol_table);
 
+    if(cmdline.isset("validate-goto-model"))
+    {
+      lazy_goto_model.validate(validation_modet::INVARIANT);
+    }
+
     // Provide show-goto-functions and similar dump functions after symex
     // executes. If --paths is active, these dump routines run after every
     // paths iteration. Its return value indicates that if we ran any dump
@@ -1141,6 +1161,7 @@ void jbmc_parse_optionst::help()
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"
+    HELP_VALIDATE
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index d5989a7a5fc..3b9d7dd30c0 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
 #define CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
 
-#include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
+#include <util/ui_message.h>
+#include <util/validation_interface.h>
 
 #include <langapi/language.h>
 
@@ -80,6 +81,7 @@ class optionst;
   "(localize-faults)(localize-faults-method):" \
   "(java-threading)" \
   OPT_GOTO_TRACE \
+  OPT_VALIDATE \
   "(symex-driven-lazy-loading)"
 // clang-format on
 
diff --git a/src/goto-programs/abstract_goto_model.h b/src/goto-programs/abstract_goto_model.h
index 6a244d837fe..25243c8f5eb 100644
--- a/src/goto-programs/abstract_goto_model.h
+++ b/src/goto-programs/abstract_goto_model.h
@@ -49,6 +49,12 @@ class abstract_goto_modelt
   /// underneath them, so this should only be used to lend a reference to code
   /// that cannot also call get_goto_function.
   virtual const symbol_tablet &get_symbol_table() const = 0;
+
+  /// Check that the goto model is well-formed
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  virtual void validate(const validation_modet vm) const = 0;
 };
 
 #endif
diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h
index a71dbf82402..3dd6e434679 100644
--- a/src/goto-programs/goto_model.h
+++ b/src/goto-programs/goto_model.h
@@ -94,7 +94,7 @@ class goto_modelt : public abstract_goto_modelt
   ///
   /// The validation mode indicates whether well-formedness check failures are
   /// reported via DATA_INVARIANT violations or exceptions.
-  void validate(const validation_modet vm) const
+  void validate(const validation_modet vm) const override
   {
     symbol_table.validate(vm);
 
@@ -138,6 +138,18 @@ class wrapper_goto_modelt : public abstract_goto_modelt
            goto_functions.function_map.end();
   }
 
+  /// Check that the goto model is well-formed
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void validate(const validation_modet vm) const override
+  {
+    symbol_table.validate(vm);
+
+    const namespacet ns(symbol_table);
+    goto_functions.validate(ns, vm);
+  }
+
 private:
   const symbol_tablet &symbol_table;
   const goto_functionst &goto_functions;
diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h
index 61b623c63ad..d62b477c838 100644
--- a/src/goto-programs/lazy_goto_model.h
+++ b/src/goto-programs/lazy_goto_model.h
@@ -243,6 +243,15 @@ class lazy_goto_modelt : public abstract_goto_modelt
     return goto_functions.at(id);
   }
 
+  /// Check that the goto model is well-formed
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void validate(const validation_modet vm) const override
+  {
+    goto_model->validate(vm);
+  }
+
 private:
   std::unique_ptr<goto_modelt> goto_model;
 
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 637715ffa04..2a947691a85 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -961,15 +961,19 @@ void symex_target_equationt::SSA_stept::validate(
   case goto_trace_stept::typet::CONSTRAINT:
     validate_full_expr(cond_expr, ns, vm);
     break;
-  case goto_trace_stept::typet::ASSIGNMENT:
   case goto_trace_stept::typet::DECL:
+    validate_full_expr(ssa_lhs, ns, vm);
+    validate_full_expr(ssa_full_lhs, ns, vm);
+    validate_full_expr(original_full_lhs, ns, vm);
+    break;
+  case goto_trace_stept::typet::ASSIGNMENT:
     validate_full_expr(ssa_lhs, ns, vm);
     validate_full_expr(ssa_full_lhs, ns, vm);
     validate_full_expr(original_full_lhs, ns, vm);
     validate_full_expr(ssa_rhs, ns, vm);
     DATA_CHECK(
       vm,
-      base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns),
+      base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns),
       "Type inequality in SSA assignment\nlhs-type: " +
         ssa_lhs.get_original_expr().type().id_string() +
         "\nrhs-type: " + ssa_rhs.type().id_string());
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 6ec29664634..d4e7058114c 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -296,14 +296,14 @@ class code_assignt:public codet
 
   static void validate(
     const codet &code,
-    const namespacet &,
+    const namespacet &ns,
     const validation_modet vm = validation_modet::INVARIANT)
   {
     check(code, vm);
 
     DATA_CHECK(
       vm,
-      code.op0().type() == code.op1().type(),
+      base_type_eq(code.op0().type(), code.op1().type(), ns),
       "lhs and rhs of assignment must have same type");
   }
 
diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp
index 58edd886cd3..73225b1e502 100644
--- a/src/util/symbol.cpp
+++ b/src/util/symbol.cpp
@@ -137,10 +137,11 @@ bool symbolt::is_well_formed() const
   // Well-formedness criterion number 2 is for a symbol
   // to have it's base name as a suffix to it's more
   // general name.
-  if(!has_suffix(id2string(name), id2string(base_name)))
-  {
+  // Exception: Java symbols' base names do not have type signatures
+  // (for example, they can have name "someclass.method:(II)V" and base name
+  // "method")
+  if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)
     return false;
-  }
 
   return true;
 }