diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
index 9f9107970bf..ff2fb37e2ef 100644
--- a/src/cbmc/all_properties.cpp
+++ b/src/cbmc/all_properties.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/time_stopping.h>
 #include <util/xml.h>
+#include <util/json.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/prop/cover_goals.h>
@@ -17,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-symex/build_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
+#include <goto-programs/json_goto_trace.h>
 
 #include "bmc.h"
 #include "bv_cbmc.h"
@@ -183,8 +185,9 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
       else if(it->source.pc->is_goto())
       {
         // this is likely an unwinding assertion
-        property_id=id2string(it->source.pc->source_location.get_function())+".unwind."+
-                    i2string(it->source.pc->loop_number);
+        property_id=id2string(
+          it->source.pc->source_location.get_function())+".unwind."+
+          i2string(it->source.pc->loop_number);
         goal_map[property_id].description=it->comment;
       }
       else
@@ -211,7 +214,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   status() << "Running " << solver.decision_procedure_text() << eom;
 
-  cover_goals();  
+  cover_goals();
 
   // output runtime
 
@@ -222,43 +225,75 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   }
   
   // report
-  if(bmc.ui!=ui_message_handlert::XML_UI)
+  switch(bmc.ui)
   {
-    status() << eom;
-    status() << "** Results:" << eom;
-  }
+    case ui_message_handlert::PLAIN:
+    {
+      status() << eom;
+      status() << "** Results:" << eom;
+      for(goal_mapt::const_iterator
+            it=goal_map.begin();
+          it!=goal_map.end();
+          it++)
+      {
+        status() << "[" << it->first << "] "
+                 << it->second.description << ": "
+                 << (it->second.failed?"FAILURE":"SUCCESS")
+                 << eom;
+      }
+      status() << eom;
   
-  for(goal_mapt::const_iterator
-      it=goal_map.begin();
-      it!=goal_map.end();
-      it++)
-  {
-    if(bmc.ui==ui_message_handlert::XML_UI)
+      status() << "** " << cover_goals.number_covered()
+               << " of " << cover_goals.size() << " failed ("
+               << cover_goals.iterations() << " iteration"
+               << (cover_goals.iterations()==1?"":"s")
+               << ")" << eom;
+      break;
+    }
+    case ui_message_handlert::XML_UI:
     {
-      xmlt xml_result("result");
-      xml_result.set_attribute("property", id2string(it->first));
-      xml_result.set_attribute("status", it->second.failed?"FAILURE":"SUCCESS");
+      for(goal_mapt::const_iterator
+            it=goal_map.begin();
+          it!=goal_map.end();
+          it++)
+      {
+        xmlt xml_result("results");
+        xml_result.set_attribute("property", id2string(it->first));
+        xml_result.set_attribute("status",
+                                 it->second.failed?"FAILURE":"SUCCESS");
 
-      if(it->second.failed)
-        convert(bmc.ns, it->second.goto_trace, xml_result.new_element());
+        if(it->second.failed)
+          convert(bmc.ns, it->second.goto_trace, xml_result.new_element());
 
-      std::cout << xml_result << "\n";
+        std::cout << xml_result << "\n";
+      }
+      break;
     }
-    else
+    case ui_message_handlert::JSON_UI:
     {
-      status() << "[" << it->first << "] "
-               << it->second.description << ": " << (it->second.failed?"FAILURE":"SUCCESS")
-               << eom;
+      json_objectt json_result;
+      json_arrayt &result_array=json_result["result"].make_array();
+      for(goal_mapt::const_iterator
+            it=goal_map.begin();
+          it!=goal_map.end();
+          it++)
+      {
+        json_objectt &result=result_array.push_back().make_object();
+        result["property"]=json_stringt(id2string(it->first));
+        result["description"]=json_stringt(id2string(it->second.description));
+        result["status"]=json_stringt(it->second.failed?"failure":"success");
+
+        if(it->second.failed)
+        {
+          jsont &json_trace=result["trace"];
+          convert(bmc.ns, it->second.goto_trace, json_trace);
+        }
+      }
+      std::cout << ",\n" << json_result;
+      break;
     }
   }
 
-  status() << eom;
-  
-  status() << "** " << cover_goals.number_covered()
-           << " of " << cover_goals.size() << " failed ("
-           << cover_goals.iterations() << " iteration"
-           << (cover_goals.iterations()==1?"":"s")
-           << ")" << eom;
 
   bool safe=(cover_goals.number_covered()==0);
 
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 1439b3cd547..5f5e17f811f 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -90,10 +90,18 @@ void bmct::error_trace()
   
   case ui_message_handlert::JSON_UI:
     {
-      json_objectt counterexample;
-      jsont &json_trace=counterexample["counterexample"];
+      json_objectt json_result;
+      json_arrayt &result_array=json_result["results"].make_array();
+      json_objectt &result=result_array.push_back().make_object();
+      const goto_trace_stept &step=goto_trace.steps.back();
+      result["property"]=
+        json_stringt(id2string(step.pc->source_location.get_property_id()));
+      result["description"]=
+        json_stringt(id2string(step.pc->source_location.get_comment()));
+      result["status"]=json_stringt("failed");
+      jsont &json_trace=result["trace"];
       convert(ns, goto_trace, json_trace);
-      std::cout << ",\n" << counterexample << "\n";
+      std::cout << ",\n" << json_result;
     }
     break;
   }
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
index c5fc0469ff1..608973e90be 100644
--- a/src/cbmc/bmc_cover.cpp
+++ b/src/cbmc/bmc_cover.cpp
@@ -11,12 +11,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/xml_expr.h>
+#include <util/json.h>
+#include <util/json_expr.h>
 
 #include <solvers/prop/cover_goals.h>
 #include <solvers/prop/literal_expr.h>
 
 #include <goto-symex/build_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
+#include <goto-programs/json_goto_trace.h>
 
 #include "bmc.h"
 #include "bv_cbmc.h"
@@ -315,60 +318,104 @@ bool bmc_covert::operator()()
   }
   
   // report
-  if(bmc.ui!=ui_message_handlert::XML_UI)
-  {
-    status() << eom;
-    status() << "** coverage results:" << eom;
-  }
-  
   unsigned goals_covered=0;
-  
-  for(const auto & it : goal_map)
+  switch(bmc.ui)
   {
-    const goalt &goal=it.second;
-    
-    if(goal.satisfied) goals_covered++;
-  
-    if(bmc.ui==ui_message_handlert::XML_UI)
+    case ui_message_handlert::PLAIN:
     {
-      xmlt xml_result("result");
-      xml_result.set_attribute("goal", id2string(it.first));
-      xml_result.set_attribute("description", goal.description);
-      xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED");
-      
-      if(goal.source_location.is_not_nil())
-        xml_result.new_element()=xml(goal.source_location);
+      status() << eom;
+      status() << "** coverage results:" << eom;
+      for(const auto & it : goal_map)
+      {
+        const goalt &goal=it.second;
 
-      if(goal.satisfied)
-        convert(bmc.ns, goal.goto_trace, xml_result.new_element());
+        if(goal.satisfied) goals_covered++;
 
-      std::cout << xml_result << "\n";
+        status() << "[" << it.first << "]";
+
+        if(goal.source_location.is_not_nil())
+          status() << ' ' << goal.source_location;
+
+        if(!goal.description.empty()) status() << ' ' << goal.description;
+
+        status() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
+                 << eom;
+      }
+      status() << eom;
+      status() << "** " << goals_covered
+               << " of " << goal_map.size() << " covered ("
+               << std::fixed << std::setw(1) << std::setprecision(1)
+               << (goal_map.empty()?0.0:100.0*goals_covered/goal_map.size())
+               << "%), using "
+               << cover_goals.iterations() << " iteration"
+               << (cover_goals.iterations()==1?"":"s")
+               << eom;
+      break;
     }
-    else
+    case ui_message_handlert::XML_UI:
     {
-      status() << "[" << it.first << "]";
+      for(const auto & it : goal_map)
+      {
+        const goalt &goal=it.second;
 
-      if(goal.source_location.is_not_nil())
-        status() << ' ' << goal.source_location;
-        
-      if(!goal.description.empty()) status() << ' ' << goal.description;
+        if(goal.satisfied) goals_covered++;
 
-      status() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
+        xmlt xml_result("result");
+        xml_result.set_attribute("goal", id2string(it.first));
+        xml_result.set_attribute("description", goal.description);
+        xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED");
+
+        if(goal.source_location.is_not_nil())
+          xml_result.new_element()=xml(goal.source_location);
+
+        if(goal.satisfied)
+          convert(bmc.ns, goal.goto_trace, xml_result.new_element());
+
+        std::cout << xml_result << "\n";
+      }
+
+      status() << eom;
+      status() << "** " << goals_covered
+               << " of " << goal_map.size() << " covered ("
+               << std::fixed << std::setw(1) << std::setprecision(1)
+               << (goal_map.empty()?0.0:100.0*goals_covered/goal_map.size())
+               << "%), using "
+               << cover_goals.iterations() << " iteration"
+               << (cover_goals.iterations()==1?"":"s")
                << eom;
+      break;
+    }
+    case ui_message_handlert::JSON_UI:
+    {
+      json_objectt json_result;
+      json_arrayt &result_array=json_result["results"].make_array();
+      for(const auto & it : goal_map)
+      {
+        const goalt &goal=it.second;
+
+        if(goal.satisfied) goals_covered++;
+
+        json_objectt &result=result_array.push_back().make_object();
+        result["status"]=json_stringt(goal.satisfied?"satisfied":"failed");
+        result["goal"]=json_stringt(id2string(it.first));
+        result["description"]=json_stringt(goal.description);
+
+        if(goal.source_location.is_not_nil())
+          result["sourceLocation"]=json(goal.source_location);
+
+        if(goal.satisfied)
+        {
+          jsont &json_trace=result["trace"];
+          convert(bmc.ns, goal.goto_trace, json_trace);
+        }
+      }
+      json_result["totalGoals"]=json_numbert(i2string(goal_map.size()));
+      json_result["goalsCovered"]=json_numbert(i2string(goals_covered));
+      std::cout << ",\n" << json_result;
+      break;
     }
   }
 
-  status() << eom;
-  
-  status() << "** " << goals_covered
-           << " of " << goal_map.size() << " covered ("
-           << std::fixed << std::setw(1) << std::setprecision(1)
-           << (goal_map.empty()?0.0:100.0*goals_covered/goal_map.size())
-           << "%), using "
-           << cover_goals.iterations() << " iteration"
-           << (cover_goals.iterations()==1?"":"s")
-           << eom;
-  
   return false;
 }
 
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
index 08a8df8598b..409e4b947fc 100644
--- a/src/goto-programs/json_goto_trace.cpp
+++ b/src/goto-programs/json_goto_trace.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening
 #include <cassert>
 
 #include <util/i2string.h>
+#include <util/json_expr.h>
 
 #include <langapi/language_util.h>
 
@@ -18,37 +19,6 @@ Author: Daniel Kroening
 
 /*******************************************************************\
 
-Function: json
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-jsont json(const source_locationt &source_location)
-{
-  json_objectt result;
-
-  if(!source_location.get_file().empty())
-    result["file"]=json_stringt(id2string(source_location.get_file()));
-
-  if(!source_location.get_line().empty())
-    result["line"]=json_numbert(id2string(source_location.get_line()));
-
-  if(!source_location.get_column().empty())
-    result["column"]=json_numbert(id2string(source_location.get_column()));
-
-  if(!source_location.get_function().empty())
-    result["function"]=json_stringt(id2string(source_location.get_function()));
-    
-  return result;
-}
-
-/*******************************************************************\
-
 Function: convert
 
   Inputs:
@@ -100,14 +70,14 @@ void convert(
       
         json_objectt &json_failure=dest_array.push_back().make_object();
         
-        json_failure["step_type"]=json_stringt("failure");
+        json_failure["stepType"]=json_stringt("failure");
         json_failure["hidden"]=jsont::json_boolean(it->hidden);
         json_failure["thread"]=json_numbert(i2string(it->thread_nr));
         json_failure["reason"]=json_stringt(id2string(it->comment));
         json_failure["property"]=json_stringt(id2string(property_id));
 
         if(!json_location.is_null())
-          json_failure["source_location"]=json_location;
+          json_failure["sourceLocation"]=json_location;
       }
       break;
       
@@ -117,10 +87,10 @@ void convert(
         irep_idt identifier=it->lhs_object.get_identifier();
         json_objectt &json_assignment=dest_array.push_back().make_object();
         
-        json_assignment["step_type"]=json_stringt("assignment");
+        json_assignment["stepType"]=json_stringt("assignment");
 
         if(!json_location.is_null())
-          json_assignment["source_location"]=json_location;
+          json_assignment["sourceLocation"]=json_location;
 
         std::string value_string, binary_string, type_string,
                     full_lhs_string, full_lhs_value_string;
@@ -155,9 +125,9 @@ void convert(
         json_assignment["hidden"]=jsont::json_boolean(it->hidden);
         json_assignment["thread"]=json_numbert(i2string(it->thread_nr));
 
-        json_assignment["assignment_type"]=
-          json_stringt(it->assignment_type==goto_trace_stept::ACTUAL_PARAMETER?"actual_parameter":
-                       "variable");
+        json_assignment["assignmentType"]=
+          json_stringt(it->assignment_type==goto_trace_stept::ACTUAL_PARAMETER?
+                       "actual-parameter":"variable");
       }
       break;
       
@@ -173,21 +143,23 @@ void convert(
     case goto_trace_stept::FUNCTION_RETURN:
       {
         std::string tag=
-          (it->type==goto_trace_stept::FUNCTION_CALL)?"function_call":"function_return";
+          (it->type==goto_trace_stept::FUNCTION_CALL)?
+            "function-call":"function-return";
         json_objectt &json_call_return=dest_array.push_back().make_object();
         
-        json_call_return["step_type"]=json_stringt(tag);
+        json_call_return["stepType"]=json_stringt(tag);
         json_call_return["hidden"]=jsont::json_boolean(it->hidden);
         json_call_return["thread"]=json_numbert(i2string(it->thread_nr));
 
         const symbolt &symbol=ns.lookup(it->identifier);
         json_objectt &json_function=json_call_return["function"].make_object();
-        json_function["display_name"]=json_stringt(id2string(symbol.display_name()));
+        json_function["displayName"]=
+          json_stringt(id2string(symbol.display_name()));
         json_function["identifier"]=json_stringt(id2string(it->identifier));
-        json_function["source_location"]=json(symbol.location);
+        json_function["sourceLocation"]=json(symbol.location);
 
         if(!json_location.is_null())
-          json_call_return["source_location"]=json_location;
+          json_call_return["sourceLocation"]=json_location;
       }
       break;
       
@@ -198,10 +170,10 @@ void convert(
         if(!json_location.is_null())
         {
           json_objectt &json_location_only=dest_array.push_back().make_object();
-          json_location_only["step_type"]=json_stringt("location-only");
+          json_location_only["stepType"]=json_stringt("location-only");
           json_location_only["hidden"]=jsont::json_boolean(it->hidden);
           json_location_only["thread"]=json_numbert(i2string(it->thread_nr));
-          json_location_only["source_location"]=json_location;
+          json_location_only["sourceLocation"]=json_location;
         }
       }
     }
diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp
index a1711491fc3..95f25ab6863 100644
--- a/src/goto-programs/loop_ids.cpp
+++ b/src/goto-programs/loop_ids.cpp
@@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/xml.h>
 #include <util/xml_expr.h>
+#include <util/json.h>
+#include <util/json_expr.h>
 #include <util/i2string.h>
 
 #include "loop_ids.h"
@@ -49,35 +51,71 @@ void show_loop_ids(
   ui_message_handlert::uit ui,
   const goto_programt &goto_program)
 {
-  for(goto_programt::instructionst::const_iterator
-      it=goto_program.instructions.begin();
-      it!=goto_program.instructions.end();
-      it++)
+  switch(ui)
   {
-    if(it->is_backwards_goto())
+    case ui_message_handlert::PLAIN:
     {
-      unsigned loop_id=it->loop_number;
+      for(goto_programt::instructionst::const_iterator
+            it=goto_program.instructions.begin();
+          it!=goto_program.instructions.end(); it++)
+      {
+        if(it->is_backwards_goto())
+        {
+          unsigned loop_id=it->loop_number;
+
+          std::cout << "Loop "
+                    << it->function << "." << loop_id << ":" << "\n";
 
-      if(ui==ui_message_handlert::XML_UI)
+          std::cout << "  " << it->source_location << "\n";
+          std::cout << "\n";
+        }
+      }
+      break;
+    }
+    case ui_message_handlert::XML_UI:
+    {
+      for(goto_programt::instructionst::const_iterator
+            it=goto_program.instructions.begin();
+          it!=goto_program.instructions.end(); it++)
       {
-        std::string id=id2string(it->function)+"."+i2string(loop_id);
+        if(it->is_backwards_goto())
+        {
+          unsigned loop_id=it->loop_number;
+          std::string id=id2string(it->function)+"."+i2string(loop_id);
       
-        xmlt xml_loop("loop");
-        xml_loop.set_attribute("name", id);
-        xml_loop.new_element("loop-id").data=id;
-        xml_loop.new_element()=xml(it->source_location);
-        std::cout << xml_loop << "\n";
+          xmlt xml_loop("loop");
+          xml_loop.set_attribute("name", id);
+          xml_loop.new_element("loop-id").data=id;
+          xml_loop.new_element()=xml(it->source_location);
+          std::cout << xml_loop << "\n";
+        }
       }
-      else if(ui==ui_message_handlert::PLAIN)
-      {
-        std::cout << "Loop "
-                  << it->function << "." << loop_id << ":" << "\n";
+      break;
+    }
+    case ui_message_handlert::JSON_UI:
+      assert(false); //use function below
+  }
+}
 
-        std::cout << "  " << it->source_location << "\n";
-        std::cout << "\n";
-      }
-      else
-        assert(false);
+void show_loop_ids_json(
+  ui_message_handlert::uit ui,
+  const goto_programt &goto_program,
+  json_arrayt &loops)
+{
+  assert(ui==ui_message_handlert::JSON_UI); //use function above
+
+  for(goto_programt::instructionst::const_iterator
+        it=goto_program.instructions.begin();
+      it!=goto_program.instructions.end(); it++)
+  {
+    if(it->is_backwards_goto())
+    {
+      unsigned loop_id=it->loop_number;
+      std::string id=id2string(it->function)+"."+i2string(loop_id);
+
+      json_objectt &loop=loops.push_back().make_object();
+      loop["name"]=json_stringt(id);
+      loop["sourceLocation"]=json(it->source_location);
     }
   }
 }
@@ -98,6 +136,21 @@ void show_loop_ids(
   ui_message_handlert::uit ui,
   const goto_functionst &goto_functions)
 {
-  forall_goto_functions(it, goto_functions)
-    show_loop_ids(ui, it->second.body);
+  switch(ui)
+  {
+    case ui_message_handlert::PLAIN:
+    case ui_message_handlert::XML_UI:
+      forall_goto_functions(it, goto_functions)
+        show_loop_ids(ui, it->second.body);
+      break;
+    case ui_message_handlert::JSON_UI:
+      json_objectt json_result;
+      json_arrayt &loops=json_result["loops"].make_array();
+
+      forall_goto_functions(it, goto_functions)
+        show_loop_ids_json(ui, it->second.body, loops);
+
+      std::cout << ",\n" << json_result;
+      break;
+  }
 }
diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp
index 324df8c91b1..49d94774e78 100644
--- a/src/goto-programs/show_properties.cpp
+++ b/src/goto-programs/show_properties.cpp
@@ -9,9 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 
 #include <util/xml.h>
+#include <util/xml_expr.h>
 #include <util/json.h>
+#include <util/json_expr.h>
 #include <util/i2string.h>
-#include <util/xml_expr.h>
 
 #include <langapi/language_util.h>
 
@@ -152,9 +153,7 @@ void show_properties_json(
       json_properties.push_back(jsont()).make_object();
     json_property["name"]=json_stringt(id2string(property_id));
     json_property["class"]=json_stringt(id2string(property_class));
-#if 0 //TODO
-    json_property["location"]=json(it->source_location);
-#endif
+    json_property["sourceLocation"]=json(it->source_location);
     json_property["description"]=json_stringt(id2string(description));
     json_property["expression"]=
       json_stringt(from_expr(ns, identifier, it->guard));
diff --git a/src/util/Makefile b/src/util/Makefile
index 6adcdd73e7c..6c1c84ff28e 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -21,7 +21,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \
       bv_arithmetic.cpp tempdir.cpp tempfile.cpp timer.cpp unicode.cpp \
       irep_ids.cpp byte_operators.cpp string2int.cpp file_util.cpp \
       memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \
-      ssa_expr.cpp
+      ssa_expr.cpp json_expr.cpp
 
 INCLUDES= -I ..
 
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
new file mode 100644
index 00000000000..f8fbcad4667
--- /dev/null
+++ b/src/util/json_expr.cpp
@@ -0,0 +1,324 @@
+/*******************************************************************\
+
+Module: Expressions in JSON
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#include "namespace.h"
+#include "expr.h"
+#include "json.h"
+#include "arith_tools.h"
+#include "ieee_float.h"
+#include "fixedbv.h"
+#include "std_expr.h"
+#include "config.h"
+#include "i2string.h"
+
+#include "json_expr.h"
+
+/*******************************************************************\
+
+Function: json
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+json_objectt json(const source_locationt &location)
+{
+  json_objectt result;
+  
+  if(!location.get_file().empty())
+    result["file"]=json_stringt(id2string(location.get_file()));
+
+  if(!location.get_line().empty())
+    result["line"]=json_stringt(id2string(location.get_line()));
+
+  if(!location.get_column().empty())
+    result["column"]=json_stringt(id2string(location.get_column()));
+
+  if(!location.get_function().empty())
+    result["function"]=json_stringt(id2string(location.get_function()));
+  
+  return result;
+}
+
+/*******************************************************************\
+
+Function: json
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+json_objectt json(
+  const typet &type,
+  const namespacet &ns)
+{
+  if(type.id()==ID_symbol)
+    return json(ns.follow(type), ns);
+
+  json_objectt result;
+
+  if(type.id()==ID_unsignedbv)
+  {
+    result["name"]=json_stringt("integer");
+    result["width"]=
+      json_numbert(i2string(to_unsignedbv_type(type).get_width()));
+  }
+  else if(type.id()==ID_signedbv)
+  {
+    result["name"]=json_stringt("integer");
+    result["width"]=json_numbert(i2string(to_signedbv_type(type).get_width()));
+  }
+  else if(type.id()==ID_floatbv)
+  {
+    result["name"]=json_stringt("float");
+    result["width"]=json_numbert(i2string(to_floatbv_type(type).get_width()));
+  }
+  else if(type.id()==ID_bv)
+  {
+    result["name"]=json_stringt("integer");
+    result["width"]=json_numbert(i2string(to_bv_type(type).get_width()));
+  }
+  else if(type.id()==ID_c_bit_field)
+  {
+    result["name"]=json_stringt("integer");
+    result["width"]=
+      json_numbert(i2string(to_c_bit_field_type(type).get_width()));
+  }
+  else if(type.id()==ID_c_enum_tag)
+  {
+    // we return the base type
+    return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns);
+  }
+  else if(type.id()==ID_fixedbv)
+  {
+    result["name"]=json_stringt("fixed");
+    result["width"]=json_numbert(i2string(to_fixedbv_type(type).get_width()));
+  }
+  else if(type.id()==ID_pointer)
+  {
+    result["name"]=json_stringt("pointer");
+    result["subtype"]=json(type.subtype(), ns);
+  }
+  else if(type.id()==ID_bool)
+  {
+    result["name"]=json_stringt("boolean");
+  }
+  else if(type.id()==ID_array)
+  {
+    result["name"]=json_stringt("array");
+    result["subtype"]=json(type.subtype(), ns);
+  }
+  else if(type.id()==ID_vector)
+  {
+    result["name"]=json_stringt("vector");
+    result["subtype"]=json(type.subtype(), ns);
+    result["size"]=json(to_vector_type(type).size(), ns);
+  }
+  else if(type.id()==ID_struct)
+  {
+    result["name"]=json_stringt("struct");
+    json_arrayt members=result["members"].make_array();
+    const union_typet::componentst &components=
+      to_union_type(type).components();
+    for(const auto & it : components)
+    {
+      json_objectt &e=members.push_back().make_object();
+      e["name"]=json_stringt(id2string(it.get_name()));
+      e["type"]=json(it.type(), ns);
+    }
+  }
+  else if(type.id()==ID_union)
+  {
+    result["name"]=json_stringt("union");
+    json_arrayt members=result["members"].make_array();
+    const union_typet::componentst &components=
+      to_union_type(type).components();
+    for(const auto & it : components)
+    {
+      json_objectt &e=members.push_back().make_object();
+      e["name"]=json_stringt(id2string(it.get_name()));
+      e["type"]=json(it.type(), ns);
+    }
+  }
+  else
+    result["name"]=json_stringt("unknown");
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: json
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+json_objectt json(
+  const exprt &expr,
+  const namespacet &ns)
+{
+  json_objectt result;
+  
+  const typet &type=ns.follow(expr.type());
+
+  if(expr.id()==ID_constant)
+  {
+    if(type.id()==ID_unsignedbv ||
+       type.id()==ID_signedbv ||
+       type.id()==ID_c_bit_field)
+    {
+      std::size_t width=to_bitvector_type(type).get_width();
+    
+      result["name"]=json_stringt("integer");
+      result["binary"]=json_stringt(expr.get_string(ID_value));
+      result["width"]=json_numbert(i2string(width));
+      
+      const typet &underlying_type=
+        type.id()==ID_c_bit_field?type.subtype():
+        type;
+
+      bool is_signed=underlying_type.id()==ID_signedbv;
+        
+      std::string sig=is_signed?"":"unsigned ";
+
+      if(width==config.ansi_c.char_width)
+        result["c_type"]=json_stringt(sig+"char");
+      else if(width==config.ansi_c.int_width)
+        result["c_type"]=json_stringt(sig+"int");
+      else if(width==config.ansi_c.short_int_width)
+        result["c_type"]=json_stringt(sig+"short int");
+      else if(width==config.ansi_c.long_int_width)
+        result["c_type"]=json_stringt(sig+"long int");
+      else if(width==config.ansi_c.long_long_int_width)
+        result["c_type"]=json_stringt(sig+"long long int");
+
+      mp_integer i;
+      if(!to_integer(expr, i))
+        result["data"]=json_stringt(integer2string(i));
+    }
+    else if(type.id()==ID_c_enum)
+    {
+      result["name"]=json_stringt("integer");
+      result["binary"]=json_stringt(expr.get_string(ID_value));
+      result["width"]=json_numbert(type.subtype().get_string(ID_width));
+      result["c_type"]=json_stringt("enum");
+
+      mp_integer i;
+      if(!to_integer(expr, i))
+        result["data"]=json_stringt(integer2string(i));
+    }
+    else if(type.id()==ID_c_enum_tag)
+    {
+      constant_exprt tmp;
+      tmp.type()=ns.follow_tag(to_c_enum_tag_type(type));
+      tmp.set_value(to_constant_expr(expr).get_value());
+      return json(tmp, ns);
+    }
+    else if(type.id()==ID_bv)
+    {
+      result["name"]=json_stringt("bitvector");
+      result["binary"]=json_stringt(expr.get_string(ID_value));
+    }
+    else if(type.id()==ID_fixedbv)
+    {
+      result["name"]=json_stringt("fixed");
+      result["width"]=json_numbert(type.get_string(ID_width));
+      result["binary"]=json_stringt(expr.get_string(ID_value));
+      result["data"]=
+        json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
+    }
+    else if(type.id()==ID_floatbv)
+    {
+      result["name"]=json_stringt("float");
+      result["width"]=json_numbert(type.get_string(ID_width));
+      result["binary"]=json_stringt(expr.get_string(ID_value));
+      result["data"]=
+        json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
+    }
+    else if(type.id()==ID_pointer)
+    {
+      result["name"]=json_stringt("pointer");
+      result["binary"]=json_stringt(expr.get_string(ID_value));
+      if(expr.get(ID_value)==ID_NULL)
+        result["data"]=json_stringt("NULL");
+    }
+    else if(type.id()==ID_bool)
+    {
+      result["name"]=json_stringt("boolean");
+      result["binary"]=json_stringt(expr.is_true()?"1":"0");
+      result["data"]=jsont::json_boolean(expr.is_true());
+    }
+    else
+    {
+      result["name"]=json_stringt("unknown");
+    }
+  }
+  else if(expr.id()==ID_array)
+  {
+    result["name"]=json_stringt("array");
+    json_arrayt elements=result["elements"].make_array();
+    
+    unsigned index=0;
+    
+    forall_operands(it, expr)
+    {
+      json_objectt &e=elements.push_back().make_object();
+      e["index"]=json_numbert(i2string(index));
+      e["value"]=json(*it, ns);
+      index++;
+    }
+  }
+  else if(expr.id()==ID_struct)
+  {
+    result["name"]=json_stringt("struct");
+    
+    // these are expected to have a struct type
+    if(type.id()==ID_struct)
+    {
+      const struct_typet &struct_type=to_struct_type(type);
+      const struct_typet::componentst &components=struct_type.components();
+      assert(components.size()==expr.operands().size());
+
+      json_arrayt members=result["members"].make_array();
+      for(unsigned m=0; m<expr.operands().size(); m++)
+      {
+        json_objectt &e=members.push_back().make_object();
+        e["value"]=json(expr.operands()[m], ns);
+        e["name"]=json_stringt(id2string(components[m].get_name()));
+      }
+    }
+  }
+  else if(expr.id()==ID_union)
+  { 
+    result["name"]=json_stringt("union");
+    
+    assert(expr.operands().size()==1);
+    
+    json_objectt &e=result["member"].make_object();
+    e["value"]=json(expr.op0(), ns);
+    e["name"]=json_stringt(id2string(to_union_expr(expr).get_component_name()));
+  }
+  else
+    result["name"]=json_stringt("unknown");
+
+  return result;
+}
+
diff --git a/src/util/json_expr.h b/src/util/json_expr.h
new file mode 100644
index 00000000000..c2f8d3b8f9a
--- /dev/null
+++ b/src/util/json_expr.h
@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module: Expressions in JSON
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#ifndef CPROVER_JSON_EXPR_H
+#define CPROVER_JSON_EXPR_H
+
+#include "json.h"
+
+class source_locationt;
+class typet;
+class exprt;
+class namespacet;
+
+json_objectt json(
+  const exprt &,
+  const namespacet &);
+
+json_objectt json(
+  const typet &,
+  const namespacet &);
+
+json_objectt json(const source_locationt &);
+
+#endif