diff --git a/examples/Benchmarks/run_solver_nuterm b/examples/Benchmarks/run_solver_nuterm
new file mode 100755
index 000000000..e60eccb18
--- /dev/null
+++ b/examples/Benchmarks/run_solver_nuterm
@@ -0,0 +1,158 @@
+#!/bin/sh
+
+set -e
+
+if false ; then
+# ok
+ebmc PWM_1.sv --solver-neural-liveness
+ebmc PWM_2.sv --solver-neural-liveness
+ebmc PWM_3.sv --solver-neural-liveness
+ebmc PWM_4.sv --solver-neural-liveness
+ebmc PWM_5.sv --solver-neural-liveness
+ebmc PWM_6.sv --solver-neural-liveness
+ebmc PWM_7.sv --solver-neural-liveness
+ebmc PWM_8.sv --solver-neural-liveness
+ebmc PWM_9.sv --solver-neural-liveness
+fi
+
+if false ; then
+# ok
+ebmc delay_1.sv --solver-neural-liveness
+ebmc delay_2.sv --solver-neural-liveness
+ebmc delay_3.sv --solver-neural-liveness
+ebmc delay_4.sv --solver-neural-liveness
+ebmc delay_5.sv --solver-neural-liveness
+ebmc delay_6.sv --solver-neural-liveness
+ebmc delay_7.sv --solver-neural-liveness
+ebmc delay_8.sv --solver-neural-liveness
+ebmc delay_9.sv --solver-neural-liveness
+ebmc delay_10.sv --solver-neural-liveness
+ebmc delay_11.sv --solver-neural-liveness
+ebmc delay_12.sv --solver-neural-liveness
+ebmc delay_13.sv --solver-neural-liveness
+ebmc delay_14.sv --solver-neural-liveness
+ebmc delay_15.sv --solver-neural-liveness
+ebmc delay_16.sv --solver-neural-liveness
+fi
+
+if false ; then
+# ok
+ebmc gray_1.sv --solver-neural-liveness
+ebmc gray_2.sv --solver-neural-liveness
+ebmc gray_3.sv --solver-neural-liveness
+ebmc gray_4.sv --solver-neural-liveness
+ebmc gray_5.sv --solver-neural-liveness
+ebmc gray_6.sv --solver-neural-liveness
+ebmc gray_7.sv --solver-neural-liveness
+ebmc gray_8.sv --solver-neural-liveness
+ebmc gray_9.sv --solver-neural-liveness
+ebmc gray_10.sv --solver-neural-liveness
+ebmc gray_11.sv --solver-neural-liveness
+fi
+
+if false ; then
+ebmc i2c_1.sv --solver-neural-liveness
+ebmc i2c_2.sv --solver-neural-liveness
+ebmc i2c_3.sv --solver-neural-liveness
+ebmc i2c_4.sv --solver-neural-liveness
+ebmc i2c_5.sv --solver-neural-liveness
+ebmc i2c_6.sv --solver-neural-liveness
+ebmc i2c_7.sv --solver-neural-liveness
+ebmc i2c_8.sv --solver-neural-liveness
+ebmc i2c_9.sv --solver-neural-liveness
+ebmc i2c_10.sv --solver-neural-liveness
+ebmc i2c_11.sv --solver-neural-liveness
+ebmc i2c_12.sv --solver-neural-liveness
+ebmc i2c_13.sv --solver-neural-liveness
+ebmc i2c_14.sv --solver-neural-liveness
+ebmc i2c_15.sv --solver-neural-liveness
+ebmc i2c_16.sv --solver-neural-liveness
+ebmc i2c_17.sv --solver-neural-liveness
+ebmc i2c_18.sv --solver-neural-liveness
+ebmc i2c_19.sv --solver-neural-liveness
+ebmc i2c_20.sv --solver-neural-liveness
+fi
+
+if false ; then
+ebmc lcd_1.sv --solver-neural-liveness "{3-state,500-cnt}"
+ebmc lcd_2.sv --solver-neural-liveness "{3-state,1000-cnt}"
+ebmc lcd_3.sv --solver-neural-liveness "{3-state,1500-cnt}"
+ebmc lcd_4.sv --solver-neural-liveness "{3-state,2500-cnt}"
+ebmc lcd_5.sv --solver-neural-liveness "{3-state,5000-cnt}"
+ebmc lcd_6.sv --solver-neural-liveness "{3-state,7500-cnt}"
+ebmc lcd_7.sv --solver-neural-liveness "{3-state,10000-cnt}"
+ebmc lcd_8.sv --solver-neural-liveness "{3-state,12500-cnt}"
+ebmc lcd_9.sv --solver-neural-liveness "{3-state,15000-cnt}"
+ebmc lcd_10.sv --solver-neural-liveness "{3-state,17500-cnt}"
+ebmc lcd_11.sv --solver-neural-liveness "{3-state,20000-cnt}"
+ebmc lcd_12.sv --solver-neural-liveness "{3-state,22500-cnt}"
+ebmc lcd_13.sv --solver-neural-liveness "{3-state,90000-cnt}"
+ebmc lcd_14.sv --solver-neural-liveness "{3-state,180000-cnt}"
+fi
+
+if false ; then
+# ok
+ebmc seven_seg_1.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_2.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_3.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_4.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_5.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_6.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_7.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_8.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_9.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_10.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_11.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_12.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_16.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_17.sv --solver-neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_18.sv --solver-neural-liveness --property SEVEN.property.p1
+fi
+
+if false ; then
+ebmc thermocouple_1.sv --solver-neural-liveness "{2-state,2**5-cnt}"
+ebmc thermocouple_2.sv --solver-neural-liveness "{2-state,2**9-cnt}"
+ebmc thermocouple_3.sv --solver-neural-liveness "{2-state,2**10-cnt}"
+ebmc thermocouple_4.sv --solver-neural-liveness "{2-state,2**10-cnt}"
+ebmc thermocouple_5.sv --solver-neural-liveness "{2-state,2**11-cnt}"
+ebmc thermocouple_6.sv --solver-neural-liveness "{2-state,2**11-cnt}"
+ebmc thermocouple_7.sv --solver-neural-liveness "{2-state,2**12-cnt}"
+ebmc thermocouple_8.sv --solver-neural-liveness "{2-state,2**12-cnt}"
+ebmc thermocouple_9.sv --solver-neural-liveness "{2-state,2**13-cnt}"
+ebmc thermocouple_10.sv --solver-neural-liveness "{2-state,2**14-cnt}"
+ebmc thermocouple_11.sv --solver-neural-liveness "{2-state,2**14-cnt}"
+ebmc thermocouple_12.sv --solver-neural-liveness "{2-state,2**14-cnt}"
+ebmc thermocouple_13.sv --solver-neural-liveness "{2-state,2**15-cnt}"
+ebmc thermocouple_14.sv --solver-neural-liveness "{2-state,2**16-cnt}"
+ebmc thermocouple_15.sv --solver-neural-liveness "{2-state,2**17-cnt}"
+ebmc thermocouple_16.sv --solver-neural-liveness "{2-state,2**18-cnt}"
+ebmc thermocouple_17.sv --solver-neural-liveness "{2-state,2**19-cnt}"
+fi
+
+if false ; then
+# ok
+ebmc uart_transmit_1.sv --solver-neural-liveness
+ebmc uart_transmit_2.sv --solver-neural-liveness
+ebmc uart_transmit_3.sv --solver-neural-liveness
+ebmc uart_transmit_4.sv --solver-neural-liveness
+ebmc uart_transmit_5.sv --solver-neural-liveness
+ebmc uart_transmit_6.sv --solver-neural-liveness
+ebmc uart_transmit_7.sv --solver-neural-liveness
+ebmc uart_transmit_8.sv --solver-neural-liveness
+ebmc uart_transmit_9.sv --solver-neural-liveness
+ebmc uart_transmit_10.sv --solver-neural-liveness
+ebmc uart_transmit_11.sv --solver-neural-liveness
+ebmc uart_transmit_12.sv --solver-neural-liveness
+fi
+
+if false ; then
+ebmc vga_1.sv --solver-neural-liveness "{2**5-v_cnt,2**7-h_cnt}"
+ebmc vga_2.sv --solver-neural-liveness "{2**6-v_cnt,2**8-h_cnt}"
+ebmc vga_3.sv --solver-neural-liveness "{2**6-v_cnt,2**8-h_cnt}"
+ebmc vga_4.sv --solver-neural-liveness "{2**7-v_cnt,2**9-h_cnt}"
+ebmc vga_5.sv --solver-neural-liveness "{2**8-v_cnt,2**9-h_cnt}"
+ebmc vga_6.sv --solver-neural-liveness "{2**8-v_cnt,2**9-h_cnt}"
+ebmc vga_7.sv --solver-neural-liveness "{2**8-v_cnt,2**10-h_cnt}"
+ebmc vga_8.sv --solver-neural-liveness "{2**9-v_cnt,2**10-h_cnt}"
+ebmc vga_9.sv --solver-neural-liveness "{2**9-v_cnt,2**11-h_cnt}"
+fi
diff --git a/regression/ebmc/solver-neural-liveness/counter1.desc b/regression/ebmc/solver-neural-liveness/counter1.desc
new file mode 100644
index 000000000..308bd0129
--- /dev/null
+++ b/regression/ebmc/solver-neural-liveness/counter1.desc
@@ -0,0 +1,9 @@
+CORE
+counter1.sv
+--traces 1 --solver-neural-liveness
+^weight: nn::fc1\.n0\.w0 = 1$
+^bias: nn::fc1\.n0\.b = .*$
+^\[main\.property\.p0\] always s_eventually main\.counter == 0: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/solver-neural-liveness/counter1.sv b/regression/ebmc/solver-neural-liveness/counter1.sv
new file mode 100644
index 000000000..774e492ac
--- /dev/null
+++ b/regression/ebmc/solver-neural-liveness/counter1.sv
@@ -0,0 +1,16 @@
+// count down from 10 to 0
+
+module main(input clk);
+
+  reg [7:0] counter;
+
+  initial counter = 10;
+
+  always @(posedge clk)
+    if(counter != 0)
+      counter = counter - 1;
+
+  // expected to pass
+  p0: assert property (s_eventually counter == 0);
+
+endmodule
diff --git a/regression/ebmc/solver-neural-liveness/wrap_around1.desc b/regression/ebmc/solver-neural-liveness/wrap_around1.desc
new file mode 100644
index 000000000..63587a300
--- /dev/null
+++ b/regression/ebmc/solver-neural-liveness/wrap_around1.desc
@@ -0,0 +1,9 @@
+CORE
+wrap_around1.sv
+--traces 1 --solver-neural-liveness
+^weight: nn::fc1\.n0\.w0 = -1$
+^bias: nn::fc1\.n0\.b = .*$
+^\[main\.property\.p0\] always s_eventually main\.counter == 10: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/solver-neural-liveness/wrap_around1.sv b/regression/ebmc/solver-neural-liveness/wrap_around1.sv
new file mode 100644
index 000000000..c18f89c68
--- /dev/null
+++ b/regression/ebmc/solver-neural-liveness/wrap_around1.sv
@@ -0,0 +1,18 @@
+// count up from 0 to 10
+
+module main(input clk);
+
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  p0: assert property (s_eventually counter == 10);
+
+endmodule
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
index 9ce056121..846cf1aa8 100644
--- a/src/ebmc/Makefile
+++ b/src/ebmc/Makefile
@@ -23,10 +23,12 @@ SRC = \
       output_verilog.cpp \
       random_traces.cpp \
       ranking_function.cpp \
+      ranking_net.cpp \
       report_results.cpp \
       show_formula_solver.cpp \
       show_properties.cpp \
       show_trans.cpp \
+      solver_neural_liveness.cpp \
       transition_system.cpp \
       waveform.cpp \
       #empty line
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index d1029b152..1b351ec0d 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "random_traces.h"
 #include "ranking_function.h"
 #include "show_trans.h"
+#include "solver_neural_liveness.h"
 
 #include <iostream>
 
@@ -162,6 +163,9 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("neural-liveness"))
       return do_neural_liveness(cmdline, ui_message_handler);
 
+    if(cmdline.isset("solver-neural-liveness"))
+      return do_solver_neural_liveness(cmdline, ui_message_handler);
+
     if(cmdline.isset("ranking-function"))
       return do_ranking_function(cmdline, ui_message_handler);
 
diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
index 29e45304e..e90093067 100644
--- a/src/ebmc/ebmc_parse_options.h
+++ b/src/ebmc/ebmc_parse_options.h
@@ -34,6 +34,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(po)(cegar)(k-induction)(2pi)(bound2):"
         "(outfile):(xml-ui)(verbosity):(gui)(json-result):"
         "(neural-liveness)(neural-engine):"
+        "(solver-neural-liveness)"
         "(reset):"
         "(version)(verilog-rtl)(verilog-netlist)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
diff --git a/src/ebmc/ebmc_solver_factory.h b/src/ebmc/ebmc_solver_factory.h
index 82915c444..7cb956bfc 100644
--- a/src/ebmc/ebmc_solver_factory.h
+++ b/src/ebmc/ebmc_solver_factory.h
@@ -16,7 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <solvers/decision_procedure.h>
 #include <solvers/prop/prop.h>
 
-#include <iosfwd>
+#include <fstream>
 #include <memory>
 
 class ebmc_solvert final
diff --git a/src/ebmc/liveness_to_safety.cpp b/src/ebmc/liveness_to_safety.cpp
index f4e78722a..fb945dff0 100644
--- a/src/ebmc/liveness_to_safety.cpp
+++ b/src/ebmc/liveness_to_safety.cpp
@@ -120,23 +120,10 @@ void liveness_to_safetyt::operator()()
   if(!properties.requires_lasso_constraints())
     return; // no
 
-  irep_idt module_identifier = transition_system.main_symbol->name;
-
   // gather the state variables
-  const namespacet ns(transition_system.symbol_table);
+  state_vars = transition_system.state_variables();
 
-  const auto &symbol_module_map =
-    transition_system.symbol_table.symbol_module_map;
-  auto lower = symbol_module_map.lower_bound(module_identifier);
-  auto upper = symbol_module_map.upper_bound(module_identifier);
-
-  for(auto it = lower; it != upper; it++)
-  {
-    const symbolt &symbol = ns.lookup(it->second);
-
-    if(symbol.is_state_var)
-      state_vars.push_back(symbol.symbol_expr());
-  }
+  const namespacet ns(transition_system.symbol_table);
 
   // create 'loop' shadow symbols for the state variables
   for(auto &symbol_expr : state_vars)
diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp
index 8def46279..8fd6838d1 100644
--- a/src/ebmc/random_traces.cpp
+++ b/src/ebmc/random_traces.cpp
@@ -84,8 +84,6 @@ class random_tracest
 
   constant_exprt random_value(const typet &);
 
-  symbolst inputs() const;
-  symbolst state_variables() const;
   symbolst remove_constrained(const symbolst &) const;
 
   void
@@ -440,80 +438,6 @@ constant_exprt random_tracest::random_value(const typet &type)
 
 /*******************************************************************\
 
-Function: random_tracest::inputs
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-random_tracest::symbolst random_tracest::inputs() const
-{
-  symbolst inputs;
-
-  const auto &module_symbol = *transition_system.main_symbol;
-
-  if(module_symbol.type.id() != ID_module)
-    throw ebmc_errort() << "expected a module but got "
-                        << module_symbol.type.id();
-
-  const auto &ports = module_symbol.type.find(ID_ports);
-
-  // filter out the inputs
-  for(auto &port : static_cast<const exprt &>(ports).operands())
-  {
-    DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol");
-    if(port.get_bool(ID_input) && !port.get_bool(ID_output))
-    {
-      symbol_exprt input_symbol(port.get(ID_identifier), port.type());
-      input_symbol.add_source_location() = port.source_location();
-      inputs.push_back(std::move(input_symbol));
-    }
-  }
-
-  return inputs;
-}
-
-/*******************************************************************\
-
-Function: random_tracest::state_variables
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-random_tracest::symbolst random_tracest::state_variables() const
-{
-  symbolst state_variables;
-
-  const auto &module_symbol = *transition_system.main_symbol;
-  const namespacet ns(transition_system.symbol_table);
-
-  const auto &symbol_module_map =
-    transition_system.symbol_table.symbol_module_map;
-  auto lower = symbol_module_map.lower_bound(module_symbol.name);
-  auto upper = symbol_module_map.upper_bound(module_symbol.name);
-
-  for(auto it = lower; it != upper; it++)
-  {
-    const symbolt &symbol = ns.lookup(it->second);
-
-    if(symbol.is_state_var)
-      state_variables.push_back(symbol.symbol_expr());
-  }
-
-  return state_variables;
-}
-
-/*******************************************************************\
-
 Function: random_tracest::remove_constrained
 
   Inputs:
@@ -665,12 +589,12 @@ void random_tracest::operator()(
     ns,
     true);
 
-  auto inputs = this->inputs();
+  auto inputs = transition_system.inputs();
 
   if(inputs.empty())
     throw ebmc_errort() << "module does not have inputs";
 
-  auto state_variables = this->state_variables();
+  auto state_variables = transition_system.state_variables();
 
   message.statistics() << "Found " << inputs.size() << " input(s) and "
                        << state_variables.size() << " state variable(s)"
diff --git a/src/ebmc/ranking_net.cpp b/src/ebmc/ranking_net.cpp
new file mode 100644
index 000000000..1b58625de
--- /dev/null
+++ b/src/ebmc/ranking_net.cpp
@@ -0,0 +1,106 @@
+/*******************************************************************\
+
+Module: Ranking Neural Net
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "ranking_net.h"
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/std_expr.h>
+
+exprt wrap_around(exprt expr)
+{
+  // map negative values to positive ones, wrap around:
+  // -1 --> int_max-1, -2 --> int_max-2, etc.
+  auto int_max = to_signedbv_type(expr.type()).largest_expr();
+  return if_exprt{sign_exprt{expr}, plus_exprt{int_max, expr}, expr};
+}
+
+tuple_exprt wrap_around_tuple(tuple_exprt expr)
+{
+  // map negative values to positive ones, wrap around:
+  // -1 --> int_max-1, -2 --> int_max-2, etc.
+  for(auto &op : expr.operands())
+    op = wrap_around(op);
+
+  return expr;
+}
+
+tuple_exprt ranking_nett::forward(const tuple_exprt &inputs) const
+{
+  auto fc1_out = fc1.forward(inputs);
+  auto w_out = wrap_around_tuple(fc1_out);
+  return w_out;
+}
+
+ranking_nett::lineart::lineart(
+  const irep_idt &__name,
+  std::size_t in,
+  std::size_t out,
+  const typet &type)
+  : name(__name)
+{
+  neurons.reserve(out);
+
+  for(std::size_t i = 0; i < out; i++)
+  {
+    irep_idt identifier = id2string(__name) + ".n" + std::to_string(i);
+    neurons.emplace_back(identifier, in, type);
+  }
+}
+
+ranking_nett::lineart::neuront::neuront(
+  const irep_idt &__name,
+  std::size_t in,
+  const typet &type)
+  : name(__name)
+{
+  {
+    irep_idt identifier = id2string(__name) + ".b";
+    bias = symbol_exprt(identifier, type);
+  }
+
+  weights.reserve(in);
+
+  for(std::size_t i = 0; i < in; i++)
+  {
+    irep_idt identifier = id2string(__name) + ".w" + std::to_string(i);
+    weights.emplace_back(symbol_exprt{identifier, type});
+  }
+}
+
+exprt ranking_nett::lineart::neuront::forward(const tuple_exprt &input) const
+{
+  exprt::operandst result;
+  result.reserve(weights.size() + 1); // one more for bias
+
+  result.push_back(bias);
+
+  PRECONDITION(weights.size() == input.operands().size());
+
+  for(std::size_t i = 0; i < weights.size(); i++)
+    result.push_back(mult_exprt{weights[i], input.operands()[i]});
+
+  return plus_exprt{std::move(result), bias.type()};
+}
+
+exprt relu(exprt expr)
+{
+  auto zero = from_integer(0, expr.type());
+  return if_exprt{greater_than_or_equal_exprt{expr, zero}, expr, zero};
+}
+
+tuple_exprt ranking_nett::lineart::forward(const tuple_exprt &input) const
+{
+  tuple_exprt::operandst result;
+  result.reserve(neurons.size());
+
+  for(auto &neuron : neurons)
+    result.push_back(neuron.forward(input));
+
+  return tuple_exprt{std::move(result)};
+}
diff --git a/src/ebmc/ranking_net.h b/src/ebmc/ranking_net.h
new file mode 100644
index 000000000..30dd4fcb9
--- /dev/null
+++ b/src/ebmc/ranking_net.h
@@ -0,0 +1,58 @@
+/*******************************************************************\
+
+Module: Ranking Neural Net
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef EBMC_RANKING_NET_H
+#define EBMC_RANKING_NET_H
+
+#include <util/mathematical_expr.h>
+
+exprt relu(exprt);
+exprt wrap_around(exprt);
+
+class ranking_nett
+{
+public:
+  explicit ranking_nett(
+    std::size_t number_of_state_variables,
+    const typet &__type)
+    : fc1("nn::fc1", number_of_state_variables, 1, __type)
+  {
+  }
+
+  tuple_exprt forward(const tuple_exprt &inputs) const;
+
+  class lineart
+  {
+  public:
+    lineart(
+      const irep_idt &name,
+      std::size_t in,
+      std::size_t out,
+      const typet &);
+
+    irep_idt name;
+
+    class neuront
+    {
+    public:
+      std::vector<exprt> weights;
+      exprt bias;
+      irep_idt name;
+      neuront(const irep_idt &name, std::size_t in, const typet &);
+      exprt forward(const tuple_exprt &) const;
+    };
+
+    std::vector<neuront> neurons;
+
+    tuple_exprt forward(const tuple_exprt &) const;
+  };
+
+  lineart fc1;
+};
+
+#endif // EBMC_RANKING_NET
diff --git a/src/ebmc/solver_neural_liveness.cpp b/src/ebmc/solver_neural_liveness.cpp
new file mode 100644
index 000000000..2ffe85dc2
--- /dev/null
+++ b/src/ebmc/solver_neural_liveness.cpp
@@ -0,0 +1,544 @@
+/*******************************************************************\
+
+Module: Solver Neural Liveness
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "solver_neural_liveness.h"
+
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
+#include <util/format_expr.h>
+#include <util/string2int.h>
+
+#include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
+#include <temporal-logic/temporal_expr.h>
+#include <verilog/sva_expr.h>
+
+#include "ebmc_error.h"
+#include "ebmc_solver_factory.h"
+#include "live_signal.h"
+#include "random_traces.h"
+#include "ranking_function.h"
+#include "ranking_net.h"
+#include "report_results.h"
+#include "waveform.h"
+
+#include <iostream>
+
+/*******************************************************************\
+
+   Class: solver_neural_livenesst
+
+ Purpose:
+
+\*******************************************************************/
+
+class solver_neural_livenesst
+{
+public:
+  solver_neural_livenesst(
+    const cmdlinet &_cmdline,
+    message_handlert &_message_handler)
+    : cmdline(_cmdline),
+      message(_message_handler),
+      solver_factory(ebmc_solver_factory(_cmdline))
+  {
+  }
+
+  int operator()();
+
+protected:
+  const cmdlinet &cmdline;
+  messaget message;
+  ebmc_solver_factoryt solver_factory;
+  transition_systemt transition_system;
+  std::vector<symbol_exprt> state_variables;
+  using state_variable_mapt = std::unordered_map<exprt, std::size_t, irep_hash>;
+  state_variable_mapt state_variable_map;
+  ebmc_propertiest properties;
+
+  using propertyt = ebmc_propertiest::propertyt;
+
+  using tracest = std::list<trans_tracet>;
+  tracest traces;
+
+  // trace state to state vector
+  tuple_exprt to_vector(const trans_tracet::statet &, const typet &) const;
+
+  exprt
+  net_to_expression(const ranking_nett &, const decision_proceduret &) const;
+
+  int show_traces();
+  void validate_properties();
+  void set_live_signal(const propertyt &, const exprt &);
+  void sample();
+  exprt guess(propertyt &);
+  void minimize(decision_proceduret &, const exprt &objective);
+  tvt verify(propertyt &, const exprt &candidate);
+};
+
+static std::unordered_map<exprt, std::size_t, irep_hash>
+to_map(const std::vector<symbol_exprt> &state_variables)
+{
+  std::unordered_map<exprt, std::size_t, irep_hash> result;
+  for(auto &v : state_variables)
+    result.emplace(v, result.size());
+  return result;
+}
+
+int solver_neural_livenesst::operator()()
+{
+  if(cmdline.isset("show-traces"))
+    return show_traces();
+
+  transition_system =
+    get_transition_system(cmdline, message.get_message_handler());
+
+  state_variables = transition_system.state_variables();
+  state_variable_map = to_map(state_variables);
+
+  // Get the properties
+  properties = ebmc_propertiest::from_command_line(
+    cmdline, transition_system, message.get_message_handler());
+
+  // Establish that the given properties are appropriate for
+  // neural liveness.
+  validate_properties();
+
+  // auto solver_factory = ebmc_solver_factory(cmdline);
+
+  // Save the transition system expression,
+  // to add the constraint for the 'live' signal.
+  const auto original_trans_expr = transition_system.main_symbol->value;
+
+  // We do everything per property.
+  for(auto &property : properties.properties)
+  {
+    if(property.is_disabled())
+      continue;
+
+    // Set the liveness signal for the property.
+    set_live_signal(property, original_trans_expr);
+
+    // Now sample some traces.
+    sample();
+
+    // Now do a guess-and-verify loop.
+    while(true)
+    {
+      const auto candidate = guess(property);
+
+      if(verify(property, candidate).is_true())
+        break; // done, property holds
+
+      const namespacet ns(transition_system.symbol_table);
+      show_waveform(property.witness_trace.value(), ns);
+
+      // record the counterexample
+      traces.push_back(property.witness_trace.value());
+    }
+  }
+
+  // report outcomes
+  const namespacet ns(transition_system.symbol_table);
+  report_results(cmdline, properties, ns, message.get_message_handler());
+  return properties.exit_code();
+}
+
+int solver_neural_livenesst::show_traces()
+{
+  transition_system =
+    get_transition_system(cmdline, message.get_message_handler());
+
+  properties = ebmc_propertiest::from_command_line(
+    cmdline, transition_system, message.get_message_handler());
+
+  validate_properties();
+
+  const auto original_trans_expr = transition_system.main_symbol->value;
+
+  for(auto &property : properties.properties)
+  {
+    if(property.is_disabled())
+      continue;
+
+    set_live_signal(property, original_trans_expr);
+
+    sample();
+
+    const namespacet ns(transition_system.symbol_table);
+
+    for(const auto &trace : traces)
+      show_trans_trace_numbered(trace, message, ns, std::cout);
+  }
+
+  return 0;
+}
+
+void solver_neural_livenesst::validate_properties()
+{
+  if(properties.properties.empty())
+    throw ebmc_errort() << "no properties";
+
+  for(auto &property : properties.properties)
+  {
+    if(property.is_disabled())
+    {
+      // ignore
+    }
+    else if(property.normalized_expr.id() == ID_AF)
+    {
+      // ok
+    }
+    else if(
+      property.normalized_expr.id() == ID_sva_always &&
+      to_sva_always_expr(property.normalized_expr).op().id() ==
+        ID_sva_s_eventually)
+    {
+      // ok
+    }
+    else
+    {
+      throw ebmc_errort()
+        << "unsupported property - only SVA s_eventually or AF implemented";
+    }
+  }
+}
+
+void solver_neural_livenesst::set_live_signal(
+  const ebmc_propertiest::propertyt &property,
+  const exprt &original_trans_expr)
+{
+  // restore the original transition system
+  auto main_symbol_writeable = transition_system.symbol_table.get_writeable(
+    transition_system.main_symbol->name);
+  main_symbol_writeable->value = original_trans_expr; // copy
+  ::set_live_signal(transition_system, property.normalized_expr);
+}
+
+void solver_neural_livenesst::sample()
+{
+  const auto number_of_traces = [this]() -> std::size_t {
+    if(cmdline.isset("traces"))
+    {
+      auto number_of_traces_opt =
+        string2optional_size_t(cmdline.get_value("traces"));
+
+      if(!number_of_traces_opt.has_value())
+        throw ebmc_errort() << "failed to parse number of traces";
+
+      return number_of_traces_opt.value();
+    }
+    else
+      return 10; // default
+  }();
+
+  const std::size_t number_of_trace_steps = [this]() -> std::size_t {
+    if(cmdline.isset("trace-steps"))
+    {
+      auto trace_steps_opt =
+        string2optional_size_t(cmdline.get_value("trace-steps"));
+
+      if(!trace_steps_opt.has_value())
+        throw ebmc_errort() << "failed to parse number of trace steps";
+
+      return trace_steps_opt.value();
+    }
+    else
+      return 10; // default
+  }();
+
+  message.status() << "Sampling " << number_of_traces << " traces with "
+                   << number_of_trace_steps << " steps" << messaget::eom;
+
+  auto trace_consumer = [&](trans_tracet trace) {
+    traces.push_back(std::move(trace));
+  };
+
+  random_traces(
+    transition_system,
+    trace_consumer,
+    number_of_traces,
+    number_of_trace_steps,
+    message.get_message_handler());
+}
+
+static bool is_live(const trans_tracet::statet &state)
+{
+  for(auto &assignment : state.assignments)
+  {
+    auto &lhs = assignment.lhs;
+    if(
+      lhs.id() == ID_symbol &&
+      to_symbol_expr(lhs).get_identifier() == "nuterm::live")
+      return assignment.rhs.is_true();
+  }
+
+  throw ebmc_errort() << "liveness signal not found";
+}
+
+static exprt loss_constraint(tuple_exprt curr, tuple_exprt next)
+{
+  PRECONDITION(curr.operands().size() == 1);
+  PRECONDITION(next.operands().size() == 1);
+
+  // The ranking needs to decrease from 'curr' to 'next'.
+  auto &curr_val = curr.operands()[0];
+  auto &next_val = next.operands()[0];
+  return less_than_exprt{next_val, curr_val};
+}
+
+tuple_exprt solver_neural_livenesst::to_vector(
+  const trans_tracet::statet &state,
+  const typet &type) const
+{
+  tuple_exprt::operandst result;
+  result.resize(state_variable_map.size(), from_integer(0, type));
+
+  for(auto &assignment : state.assignments)
+  {
+    auto s_it = state_variable_map.find(assignment.lhs);
+    if(s_it != state_variable_map.end())
+      if(assignment.rhs.is_constant())
+        result[s_it->second] =
+          typecast_exprt::conditional_cast(assignment.rhs, type);
+  }
+
+  return tuple_exprt{std::move(result)};
+}
+
+static exprt objective(const ranking_nett &net)
+{
+  // return from_integer(0, signedbv_typet{32});
+
+  exprt::operandst summands;
+
+  for(auto &neuron : net.fc1.neurons)
+  {
+    for(auto &weight : neuron.weights)
+      summands.push_back(abs_exprt{weight});
+
+    // summands.push_back(abs_exprt{neuron.bias});
+  }
+
+  DATA_INVARIANT(!summands.empty(), "must have neuron");
+  auto type = summands[0].type();
+
+  return plus_exprt{std::move(summands), std::move(type)};
+}
+
+void solver_neural_livenesst::minimize(
+  decision_proceduret &solver,
+  const exprt &objective)
+{
+  exprt objective_value = nil_exprt();
+
+  std::size_t iteration = 0;
+  while(true)
+  {
+    iteration++;
+    message.status() << "iteration " << iteration << messaget::eom;
+
+    // we want a better solution
+    auto constraint = objective_value.is_nil()
+                        ? static_cast<exprt>(true_exprt())
+                        : less_than_exprt{objective, objective_value};
+
+    auto dec_result = solver(constraint);
+
+    switch(dec_result)
+    {
+    case decision_proceduret::resultt::D_SATISFIABLE:
+      objective_value = solver.get(objective);
+      message.status() << "objective: " << format(objective_value)
+                       << messaget::eom;
+      break;
+
+    case decision_proceduret::resultt::D_UNSATISFIABLE:
+      if(objective_value.is_nil())
+      {
+        // no ranking function possible
+        throw ebmc_errort()
+          << "architecture does not allow ranking function, giving up";
+      }
+
+      message.status() << "found optimal assignment" << messaget::eom;
+
+      // go back to previous, to get satisfying assignment
+      solver(equal_exprt{objective, objective_value});
+      return;
+
+    case decision_proceduret::resultt::D_ERROR:
+      throw ebmc_errort() << "Error from decision procedure";
+
+    default:
+      throw ebmc_errort() << "Unexpected result from decision procedure";
+    }
+  }
+}
+
+static void bits_constraint(
+  const exprt &expr,
+  std::size_t bits,
+  decision_proceduret &solver)
+{
+  PRECONDITION(bits != 0);
+
+  auto expr_bits = to_bitvector_type(expr.type()).get_width();
+
+  if(expr_bits <= bits)
+    return; // nothing to do
+
+  // signed encoding
+  auto top_bit = extractbit_exprt{expr, expr_bits - 1};
+
+  for(std::size_t i = bits; i < expr_bits - 1; i++)
+    solver << equal_exprt{top_bit, extractbit_exprt{expr, i}};
+}
+
+exprt solver_neural_livenesst::net_to_expression(
+  const ranking_nett &net,
+  const decision_proceduret &solver) const
+{
+  // get the weights
+  for(auto &weight : net.fc1.neurons[0].weights)
+    std::cout << "weight: " << format(weight) << " = "
+              << format(solver.get(weight)) << '\n';
+
+  // get the bias
+  auto &bias = net.fc1.neurons[0].bias;
+  std::cout << "bias: " << format(bias) << " = " << format(solver.get(bias))
+            << '\n';
+
+  exprt::operandst summands;
+
+  for(std::size_t i = 0; i < state_variables.size(); i++)
+  {
+    auto weight_value = solver.get(net.fc1.neurons[0].weights[i]);
+    if(!weight_value.is_zero())
+      summands.push_back(mult_exprt{
+        weight_value,
+        typecast_exprt::conditional_cast(
+          state_variables[i], weight_value.type())});
+  }
+
+  if(!solver.get(bias).is_zero())
+    summands.push_back(solver.get(bias));
+
+  if(summands.empty())
+    throw ebmc_errort() << "no weights";
+
+  exprt fc1;
+
+  if(summands.size() == 1)
+    fc1 = summands.front();
+  else
+  {
+    auto type = summands.front().type();
+    fc1 = plus_exprt{std::move(summands), std::move(type)};
+  }
+
+  return wrap_around(fc1);
+}
+
+exprt solver_neural_livenesst::guess(propertyt &property)
+{
+  message.status() << "Fitting a ranking function" << messaget::eom;
+
+  const namespacet ns(transition_system.symbol_table);
+  satcheckt satcheck{message.get_message_handler()};
+  boolbvt solver(ns, satcheck, message.get_message_handler());
+  //auto solver_container = solver_factory(ns, message.get_message_handler());
+  //auto &solver = solver_container.decision_procedure();
+
+  // set up net
+  auto net_type = signedbv_typet{40};
+  auto net = ranking_nett{state_variable_map.size(), net_type};
+
+  // form a batch
+  std::size_t transitions = 0;
+
+  for(const auto &trace : traces)
+  {
+    for(std::size_t i = 1; i < trace.states.size(); i++)
+    {
+      auto &curr = trace.states[i - 1];
+      auto &next = trace.states[i];
+
+      if(is_live(curr) || is_live(next))
+        continue;
+
+      auto prediction_curr = net.forward(to_vector(curr, net_type));
+      auto prediction_next = net.forward(to_vector(next, net_type));
+
+      // loss must be zero
+      solver << loss_constraint(
+        std::move(prediction_curr), std::move(prediction_next));
+
+      transitions++;
+    }
+  }
+
+  message.status() << "Batch with " << transitions << " transition(s)"
+                   << messaget::eom;
+
+  // constraints on parameters
+  for(auto &weight : net.fc1.neurons[0].weights)
+    bits_constraint(weight, 2, solver);
+
+  // get the bias
+  bits_constraint(net.fc1.neurons[0].bias, 35, solver);
+
+  // minimize
+  auto objective = ::objective(net);
+  message.status() << format(objective) << messaget::eom;
+  const auto objective_symbol =
+    symbol_exprt{"nuterm::objective", objective.type()};
+  solver << equal_exprt{objective_symbol, std::move(objective)};
+  solver.set_frozen(solver.convert_bv(objective_symbol));
+  minimize(solver, objective_symbol);
+
+  // read off the candidate
+  exprt candidate = net_to_expression(net, solver);
+
+  message.status() << "candidate: " << messaget::green << format(candidate)
+                   << messaget::reset << messaget::eom;
+
+  return candidate;
+}
+
+tvt solver_neural_livenesst::verify(
+  ebmc_propertiest::propertyt &property,
+  const exprt &candidate)
+{
+  message.status() << "Checking the candidate ranking function"
+                   << messaget::eom;
+
+  auto result = is_ranking_function(
+    transition_system,
+    property.normalized_expr,
+    candidate,
+    solver_factory,
+    message.get_message_handler());
+
+  property.witness_trace = std::move(result.second);
+
+  if(result.first.is_true())
+    property.proved();
+  else
+    property.inconclusive();
+
+  return result.first;
+}
+
+int do_solver_neural_liveness(
+  const cmdlinet &cmdline,
+  ui_message_handlert &ui_message_handler)
+{
+  return solver_neural_livenesst(cmdline, ui_message_handler)();
+}
diff --git a/src/ebmc/solver_neural_liveness.h b/src/ebmc/solver_neural_liveness.h
new file mode 100644
index 000000000..c639c1d6b
--- /dev/null
+++ b/src/ebmc/solver_neural_liveness.h
@@ -0,0 +1,17 @@
+/*******************************************************************\
+
+Module: Solver Neural Liveness
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef EBMC_SOLVER_NEURAL_LIVENESS_H
+#define EBMC_SOLVER_NEURAL_LIVENESS_H
+
+#include <util/cmdline.h>
+#include <util/ui_message.h>
+
+int do_solver_neural_liveness(const cmdlinet &, ui_message_handlert &);
+
+#endif // EBMC_SOLVER_NEURAL_LIVENESS_H
diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp
index 3ebacd496..dcbf8d54b 100644
--- a/src/ebmc/transition_system.cpp
+++ b/src/ebmc/transition_system.cpp
@@ -368,3 +368,53 @@ int show_symbol_table(
   return get_transition_system(
     cmdline, message_handler, dummy_transition_system);
 }
+
+std::vector<symbol_exprt> transition_systemt::state_variables() const
+{
+  std::vector<symbol_exprt> state_variables;
+
+  const auto &module_symbol = *main_symbol;
+  const namespacet ns(symbol_table);
+
+  const auto &symbol_module_map = symbol_table.symbol_module_map;
+  auto lower = symbol_module_map.lower_bound(module_symbol.name);
+  auto upper = symbol_module_map.upper_bound(module_symbol.name);
+
+  for(auto it = lower; it != upper; it++)
+  {
+    const symbolt &symbol = ns.lookup(it->second);
+
+    if(symbol.is_state_var)
+      state_variables.push_back(symbol.symbol_expr());
+  }
+
+  return state_variables;
+}
+
+std::vector<symbol_exprt> transition_systemt::inputs() const
+{
+  std::vector<symbol_exprt> inputs;
+
+  const auto &module_symbol = *main_symbol;
+
+  DATA_INVARIANT(
+    module_symbol.type.id() == ID_module, "main_symbol must be module");
+
+  const auto &ports_irep = module_symbol.type.find(ID_ports);
+
+  // filter out the inputs
+  auto &ports = static_cast<const exprt &>(ports_irep).operands();
+  for(auto &port : ports)
+  {
+    DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol");
+    if(port.get_bool(ID_input) && !port.get_bool(ID_output))
+    {
+      symbol_exprt input_symbol(
+        to_symbol_expr(port).get_identifier(), port.type());
+      input_symbol.add_source_location() = port.source_location();
+      inputs.push_back(std::move(input_symbol));
+    }
+  }
+
+  return inputs;
+}
diff --git a/src/ebmc/transition_system.h b/src/ebmc/transition_system.h
index eb7501eb2..a2451632e 100644
--- a/src/ebmc/transition_system.h
+++ b/src/ebmc/transition_system.h
@@ -29,6 +29,9 @@ class transition_systemt
   transt trans_expr; // transition system expression
 
   void output(std::ostream &) const;
+
+  std::vector<symbol_exprt> state_variables() const;
+  std::vector<symbol_exprt> inputs() const;
 };
 
 transition_systemt get_transition_system(const cmdlinet &, message_handlert &);