diff --git a/regression/test_gen/java1/A.class b/regression/test_gen/java1/A.class
new file mode 100644
index 00000000000..ae8d8c46f5c
Binary files /dev/null and b/regression/test_gen/java1/A.class differ
diff --git a/regression/test_gen/java1/B.class b/regression/test_gen/java1/B.class
new file mode 100644
index 00000000000..f95ad8f60fe
Binary files /dev/null and b/regression/test_gen/java1/B.class differ
diff --git a/regression/test_gen/java1/C.class b/regression/test_gen/java1/C.class
new file mode 100644
index 00000000000..eaac34051b6
Binary files /dev/null and b/regression/test_gen/java1/C.class differ
diff --git a/regression/test_gen/java1/TestGenTest.class b/regression/test_gen/java1/TestGenTest.class
new file mode 100644
index 00000000000..e44f55065a3
Binary files /dev/null and b/regression/test_gen/java1/TestGenTest.class differ
diff --git a/regression/test_gen/java1/TestGenTest.java b/regression/test_gen/java1/TestGenTest.java
new file mode 100644
index 00000000000..9854fa8e9d4
--- /dev/null
+++ b/regression/test_gen/java1/TestGenTest.java
@@ -0,0 +1,55 @@
+class A
+{
+  public int a_field_0;
+  public int a_field_1;
+
+  public A(int a_field_0)
+  {
+    this.a_field_0=a_field_0;
+  }
+}
+
+class B extends A
+{
+  public int b_field_0;
+
+  public B()
+  {
+    super(999);
+  }
+}
+
+class C
+{
+  public int c_field_0;
+  public B c_field_1;
+
+  public C(int c_field_0, B c_field_1)
+  {
+    this.c_field_0=c_field_0;
+    this.c_field_1=c_field_1;
+  }
+}
+
+public class TestGenTest
+{
+  public static void f(B param0, C param1, int param2)
+  {
+    int a_field_0=param0.a_field_0;
+    int a_field_1=param0.a_field_1;
+    int b_field_0=param0.b_field_0;
+    int c_field_0=param1.c_field_0;
+    int c_field_1_a_field_0=param1.c_field_1.a_field_0;
+    int c_field_1_a_field_1=param1.c_field_1.a_field_1;
+    int c_field_1_b_field_0=param1.c_field_1.b_field_0;
+
+    assert a_field_0           != 499 ||
+           a_field_1           != 498 ||
+           b_field_0           != 497 ||
+           c_field_0           != 496 ||
+           c_field_1_a_field_0 != 495 ||
+           c_field_1_a_field_1 != 494 ||
+           c_field_1_b_field_0 != 493 ||
+           param2              != 492;
+  }
+}
diff --git a/regression/test_gen/java1/test.desc b/regression/test_gen/java1/test.desc
new file mode 100644
index 00000000000..ec1e73a6ed7
--- /dev/null
+++ b/regression/test_gen/java1/test.desc
@@ -0,0 +1,9 @@
+CORE
+TestGenTest.class
+--gen-java-test-case --function TestGenTest.f
+^EXIT=0$
+^SIGNAL=0$
+^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
+--
+^warning: ignoring
diff --git a/regression/test_gen/primitive1/TestGenTest.class b/regression/test_gen/primitive1/TestGenTest.class
new file mode 100644
index 00000000000..e13e8312110
Binary files /dev/null and b/regression/test_gen/primitive1/TestGenTest.class differ
diff --git a/regression/test_gen/primitive1/TestGenTest.java b/regression/test_gen/primitive1/TestGenTest.java
new file mode 100644
index 00000000000..f537a25ecc5
--- /dev/null
+++ b/regression/test_gen/primitive1/TestGenTest.java
@@ -0,0 +1,7 @@
+public class TestGenTest
+{
+  public static void main(int param_0, int param_1)
+  {
+    assert param_0 != 499 && param_1 != 498;
+  }
+}
diff --git a/regression/test_gen/primitive1/test.desc b/regression/test_gen/primitive1/test.desc
new file mode 100644
index 00000000000..14c448f7cf4
--- /dev/null
+++ b/regression/test_gen/primitive1/test.desc
@@ -0,0 +1,9 @@
+CORE
+TestGenTest.class
+--gen-java-test-case
+^EXIT=0$
+^SIGNAL=0$
+^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
+--
+^warning: ignoring
diff --git a/src/Makefile b/src/Makefile
index 1db144e1da7..bbb202de7c2 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,7 +1,7 @@
 DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
        goto-symex langapi pointer-analysis solvers util linking xmllang \
        assembler analyses java_bytecode aa-path-symex path-symex musketeer \
-       json cegis goto-analyzer jsil symex
+       json cegis goto-analyzer jsil symex test_gen
 
 all: cbmc.dir goto-cc.dir goto-instrument.dir symex.dir goto-analyzer.dir
 
@@ -29,7 +29,7 @@ musketeer.dir: goto-instrument.dir
 
 cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
-          goto-instrument.dir
+          goto-instrument.dir test_gen.dir
 
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    json.dir goto-instrument.dir
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index a09e849017e..1be0899ba44 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -25,6 +25,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
+      ../test_gen/test_gen$(LIBEXT) \
       ../util/util$(LIBEXT)
 
 INCLUDES= -I ..
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index e7eb872bef4..2605e8c8f90 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -46,6 +46,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <pointer-analysis/add_failed_symbols.h>
 
+#include <test_gen/java_test_case_generator.h>
+
 #include <analyses/goto_check.h>
 
 #include <langapi/mode.h>
@@ -445,6 +447,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("graphml-cex"))
     options.set_option("graphml-cex", cmdline.get_value("graphml-cex"));
+
+  if(cmdline.isset("gen-java-test-case"))
+    options.set_option("gen-java-test-case", true);
 }
 
 /*******************************************************************\
@@ -561,6 +566,9 @@ int cbmc_parse_optionst::doit()
   if(set_properties(goto_functions))
     return 7;
 
+  if(options.get_bool_option("gen-java-test-case"))
+    return generate_java_test_case(options, symbol_table, goto_functions, bmc);
+
   // do actual BMC
   return do_bmc(bmc, goto_functions);
 }
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index f1662fbfece..6643ed973e9 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -53,6 +53,7 @@ class optionst;
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-cex):" \
+  "(gen-java-test-case)(test_case_file):"\
   "(floatbv)(all-claims)(all-properties)(decide)" // legacy, and will eventually disappear
 
 class cbmc_parse_optionst:
diff --git a/src/test_gen/Makefile b/src/test_gen/Makefile
new file mode 100644
index 00000000000..26bd09b1dc4
--- /dev/null
+++ b/src/test_gen/Makefile
@@ -0,0 +1,16 @@
+SRC = java_test_case_generator.cpp java_test_source_factory.cpp
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = test_gen$(LIBEXT)
+
+all: test_gen$(LIBEXT)
+
+###############################################################################
+
+test_gen$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+
diff --git a/src/test_gen/java_test_case_generator.cpp b/src/test_gen/java_test_case_generator.cpp
new file mode 100644
index 00000000000..1d943b5d741
--- /dev/null
+++ b/src/test_gen/java_test_case_generator.cpp
@@ -0,0 +1,107 @@
+#include <iostream>
+#include <functional>
+
+#include <util/message.h>
+#include <cbmc/bmc.h>
+
+#include <java_bytecode/java_entry_point.h>
+#include <test_gen/java_test_source_factory.h>
+#include <test_gen/java_test_case_generator.h>
+
+namespace
+{
+bool is_meta(const irep_idt &id)
+{
+  const std::string &n=id2string(id);
+  return std::string::npos != n.find("$assertionsDisabled")
+      || std::string::npos != n.find("tmp_struct_init$");
+}
+
+inputst generate_inputs(const symbol_tablet &st, const goto_functionst &gf,
+    const goto_tracet &trace)
+{
+  std::map<const irep_idt, exprt> result;
+  for (const goto_trace_stept &step : trace.steps)
+  {
+    if (goto_trace_stept::ASSIGNMENT == step.type)
+    {
+      const exprt &lhs=step.full_lhs;
+      if (ID_symbol == lhs.id())
+      {
+        const irep_idt &id=to_symbol_expr(lhs).get_identifier();
+        if (st.has_symbol(id) && !is_meta(id))
+        {
+          const exprt &value=step.full_lhs_value;
+          result.insert(std::make_pair(id, value));
+        }
+      }
+    }
+  }
+  return result;
+}
+
+const irep_idt &get_entry_function_id(const goto_functionst &gf)
+{
+  typedef goto_functionst::function_mapt function_mapt;
+  const function_mapt &fm=gf.function_map;
+  const irep_idt start(goto_functionst::entry_point());
+  const function_mapt::const_iterator entry_func=fm.find(start);
+  assert(fm.end() != entry_func);
+  const goto_programt::instructionst &in=entry_func->second.body.instructions;
+  typedef goto_programt::instructionst::const_reverse_iterator reverse_target;
+  const reverse_target last=in.rbegin();
+  const reverse_target end=in.rend();
+  assert(end != last);
+  const reverse_target call=std::next(last);
+  assert(end != call);
+  const code_function_callt &func_call=to_code_function_call(call->code);
+  const exprt &func_expr=func_call.function();
+  return to_symbol_expr(func_expr).get_identifier();
+}
+
+typedef std::function<
+    std::string(const symbol_tablet &, const irep_idt &, const inputst &)> test_case_generatort;
+
+int generate_test_case(optionst &options, const symbol_tablet &st,
+    const goto_functionst &gf, bmct &bmc, const test_case_generatort generate)
+{
+  options.set_option("stop-on-fail", true);
+  switch (bmc(gf))
+  {
+  case safety_checkert::SAFE:
+    return TEST_CASE_FAIL;
+  case safety_checkert::ERROR:
+    return TEST_CASE_ERROR;
+  case safety_checkert::UNSAFE:
+  default:
+  {
+    const goto_tracet &trace=bmc.safety_checkert::error_trace;
+    const inputst inputs(generate_inputs(st, gf, trace));
+    const irep_idt &entry_func_id=get_entry_function_id(gf);
+    const std::string source(generate(st, entry_func_id, inputs));
+    const std::string file(options.get_option("test_case_file"));
+    if (file.empty()) std::cout << source;
+    else
+    {
+      std::ofstream ofs(file.c_str());
+      ofs << source;
+    }
+    return TEST_CASE_SUCCESS;
+  }
+  }
+}
+}
+
+int generate_java_test_case(optionst &o, const symbol_tablet &st,
+    const goto_functionst &gf, bmct &bmc)
+{
+  try
+  {
+    return generate_test_case(o, st, gf, bmc,
+        generate_java_test_case_from_inputs);
+  } catch (const std::string &ex)
+  {
+    std::cerr << ex << std::endl;
+    throw;
+  }
+}
diff --git a/src/test_gen/java_test_case_generator.h b/src/test_gen/java_test_case_generator.h
new file mode 100644
index 00000000000..f903811442c
--- /dev/null
+++ b/src/test_gen/java_test_case_generator.h
@@ -0,0 +1,33 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, kroening@kroening.com
+         Pascal Kesseli, pascal.kesseil@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#ifndef JAVA_TEST_CASE_GENERATOR_H_
+#define JAVA_TEST_CASE_GENERATOR_H_
+
+#define TEST_CASE_SUCCESS 0
+#define TEST_CASE_FAIL 1
+#define TEST_CASE_ERROR 10
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param options
+ * @param st
+ * @param gf
+ * @param bmc
+ */
+int generate_java_test_case(
+    class optionst &options,
+    const class symbol_tablet &st,
+    const class goto_functionst &gf,
+    class bmct &bmc);
+
+#endif /* JAVA_TEST_CASE_GENERATOR_H_ */
diff --git a/src/test_gen/java_test_source_factory.cpp b/src/test_gen/java_test_source_factory.cpp
new file mode 100644
index 00000000000..6ee94ccace6
--- /dev/null
+++ b/src/test_gen/java_test_source_factory.cpp
@@ -0,0 +1,226 @@
+#include <algorithm>
+#include <set>
+
+#include <util/substitute.h>
+#include <util/std_types.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+#include <util/namespace.h>
+
+#include <java_bytecode/expr2java.h>
+
+#include <test_gen/java_test_source_factory.h>
+
+#define INDENT_SPACES "  "
+#define JAVA_NS_PREFIX_LEN 6u
+
+namespace
+{
+std::string &indent(std::string &result, const size_t num_indent=1u)
+{
+  for (size_t i=0u; i < num_indent; ++i)
+    result+=INDENT_SPACES;
+  return result;
+}
+
+void add_test_class_name(std::string &result, const std::string &func_name)
+{
+  result+="class ";
+  result+=func_name;
+  result+="Test {\n";
+  indent(result)+="public void test";
+  result+=func_name;
+  result+="() {\n";
+}
+
+void add_symbol(std::string &result, const symbolt &s)
+{
+  // XXX: Should be expr2java(...) once functional.
+  const irep_idt &n=s.pretty_name.empty() ? s.base_name : s.pretty_name;
+  result+=id2string(n);
+}
+
+void add_qualified_class_name(std::string &result, const namespacet &ns,
+    const typet &type)
+{
+  if (ID_symbol == type.id())
+  {
+    const std::string &id=id2string(to_symbol_type(type).get_identifier());
+    assert(id.size() >= JAVA_NS_PREFIX_LEN);
+    result+=id.substr(JAVA_NS_PREFIX_LEN);
+  } else result+=id2string(to_struct_type(type).get_tag());
+}
+
+void add_decl_with_init_prefix(std::string &result, const symbol_tablet &st,
+    const symbolt &symbol)
+{
+  const namespacet ns(st);
+  if (ID_pointer != symbol.type.id()) result+=type2java(symbol.type, ns);
+  else add_qualified_class_name(result, ns, symbol.type.subtype());
+  result+=' ';
+}
+
+void add_value(std::string &result, const symbol_tablet &st,
+    const struct_exprt &value, const std::string &this_name);
+
+void add_value(std::string &result, const symbol_tablet &st, const exprt &value,
+    const std::string var_name="")
+{
+  const namespacet ns(st);
+  const irep_idt &id=value.id();
+  if (ID_address_of == id) add_value(result, st,
+      to_address_of_expr(value).object());
+  else if (ID_struct == id) add_value(result, st, to_struct_expr(value),
+      var_name);
+  else result+=expr2java(value, ns);
+}
+
+class member_factoryt
+{
+  std::string &result;
+  const symbol_tablet &st;
+  const std::string &this_name;
+  const struct_typet::componentst &comps;
+  size_t comp_index;
+
+public:
+  member_factoryt(std::string &result, const symbol_tablet &st,
+      const std::string &this_name, const typet &type) :
+      result(result), st(st), this_name(this_name), comps(
+          to_struct_type(type).components()), comp_index(0u)
+  {
+  }
+
+  void operator()(const exprt &value)
+  {
+    assert(comp_index < comps.size());
+    if (ID_struct == value.id())
+    {
+      member_factoryt mem_fac(result, st, this_name, value.type());
+      const struct_exprt::operandst &ops=value.operands();
+      std::for_each(ops.begin(), ops.end(), mem_fac);
+      if (comp_index < comps.size() - 1) result+=";\n";
+    } else
+    {
+      const struct_typet::componentt &comp=comps[comp_index];
+      if (ID_symbol != comp.type().id())
+      {
+        indent(result, 2u)+="Reflector.setInstanceField(";
+        result+=this_name;
+        result+=",\"";
+        result+=id2string(comp.get_pretty_name());
+        result+="\",";
+        add_value(result, st, value);
+        result+=")";
+        if (comp_index < comps.size() - 1) result+=";\n";
+      }
+    }
+    ++comp_index;
+  }
+};
+
+void add_value(std::string &result, const symbol_tablet &st,
+    const struct_exprt &value, const std::string &this_name)
+{
+  const namespacet ns(st);
+  result+='(';
+  const typet &type=value.type();
+  add_qualified_class_name(result, ns, type);
+  result+=") Reflector.forceInstance(\"";
+  add_qualified_class_name(result, ns, type);
+  result+="\");\n";
+  member_factoryt mem_fac(result, st, this_name, type);
+  const struct_exprt::operandst &ops=value.operands();
+  std::for_each(ops.begin(), ops.end(), mem_fac);
+}
+
+void add_assign_value(std::string &result, const symbol_tablet &st,
+    const symbolt &symbol, const exprt &value)
+{
+  std::string symbol_name;
+  add_symbol(symbol_name, symbol);
+  result+=symbol_name;
+  result+='=';
+  add_value(result, st, value, symbol_name);
+  result+=";\n";
+}
+
+void add_global_state_assignments(std::string &result, const symbol_tablet &st,
+    inputst &inputs)
+{
+  for (inputst::value_type &input : inputs)
+  {
+    const symbolt &symbol=st.lookup(input.first);
+    if (!symbol.is_static_lifetime) continue;
+    add_assign_value(indent(result, 2u), st, symbol, input.second);
+  }
+}
+
+std::set<irep_idt> get_parameters(const symbolt &func)
+{
+  std::set<irep_idt> result;
+  const code_typet &code_type=to_code_type(func.type);
+  const code_typet::parameterst &params=code_type.parameters();
+  for (const code_typet::parametert &param : params)
+    result.insert(param.get_identifier());
+  return result;
+}
+
+void add_func_call_parameters(std::string &result, const symbol_tablet &st,
+    const irep_idt &func_id, inputst &inputs)
+{
+  const symbolt &func=st.lookup(func_id);
+  const std::set<irep_idt> params(get_parameters(func));
+  for (const irep_idt &param : params)
+  {
+    const symbolt &symbol=st.lookup(param);
+    const inputst::iterator value=inputs.find(param);
+    assert(inputs.end() != value);
+    add_decl_with_init_prefix(indent(result, 2u), st, symbol);
+    add_assign_value(result, st, symbol, value->second);
+  }
+}
+
+std::string &add_func_call(std::string &result, const symbol_tablet &st,
+    const irep_idt &func_id)
+{
+  // XXX: Should be expr2java(...) once functional.
+  const symbolt &s=st.lookup(func_id);
+  const std::string func_name_with_brackets(id2string(s.pretty_name));
+  const size_t sz=func_name_with_brackets.size();
+  assert(sz >= 2u);
+  indent(result, 2u)+=func_name_with_brackets.substr(0, sz - 2);
+  result+='(';
+  const std::set<irep_idt> params(get_parameters(s));
+  for (const irep_idt &param : params)
+  {
+    add_symbol(result, st.lookup(param));
+    result+=',';
+  }
+  *result.rbegin()=')';
+  result+=";\n";
+  indent(result)+="}\n";
+  return result+="}\n";
+}
+
+std::string get_escaped_func_name(const symbolt &symbol)
+{
+  std::string result(id2string(symbol.pretty_name));
+  substitute(result, ".", "_");
+  substitute(result, "(", "X");
+  substitute(result, ")", "Y");
+  return result;
+}
+}
+
+std::string generate_java_test_case_from_inputs(const symbol_tablet &st,
+    const irep_idt &func_id, inputst inputs)
+{
+  const symbolt &func=st.lookup(func_id);
+  const std::string func_name(get_escaped_func_name(func));
+  std::string result;
+  add_test_class_name(result, func_name);
+  add_global_state_assignments(result, st, inputs);
+  add_func_call_parameters(result, st, func_id, inputs);
+  return add_func_call(result, st, func_id);
+}
diff --git a/src/test_gen/java_test_source_factory.h b/src/test_gen/java_test_source_factory.h
new file mode 100644
index 00000000000..46be02cdad6
--- /dev/null
+++ b/src/test_gen/java_test_source_factory.h
@@ -0,0 +1,38 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, kroening@kroening.com
+         Pascal Kesseli, pascal.kesseil@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#ifndef JAVA_TEST_SOURCE_FACTORY_H_
+#define JAVA_TEST_SOURCE_FACTORY_H_
+
+#include <util/expr.h>
+
+/**
+ * @brief
+ *
+ * @details
+ */
+typedef std::map<const irep_idt, exprt> inputst;
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param st
+ * @param func_id
+ * @param inputs
+ *
+ * @return
+ */
+std::string generate_java_test_case_from_inputs(
+    const class symbol_tablet &st,
+    const irep_idt &func_id,
+    inputst inputs);
+
+#endif /* JAVA_TEST_SOURCE_FACTORY_H_ */