fx

Author: kroening

regression/ebmc/neural-liveness/counter1.desc

@@ -1,6 +1,6 @@
 CORE
 counter1.sv
---number-of-traces 2 --neural-liveness --neural-engine "echo Candidate: counter\\\\n"
+--number-of-traces 2 --neural-liveness --neural-engine "echo RESULT: counter\\\\n"
 ^\[main\.property\.p0\] always s_eventually main.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$

regression/ebmc/neural-liveness/live_signal1.desc

@@ -1,17 +1,17 @@
 CORE
 counter1.sv
 --number-of-traces 1 --neural-liveness --show-traces
-^nuterm::live@0 = 0$
-^nuterm::live@1 = 0$
-^nuterm::live@2 = 0$
-^nuterm::live@3 = 0$
-^nuterm::live@4 = 0$
-^nuterm::live@5 = 0$
-^nuterm::live@6 = 0$
-^nuterm::live@7 = 0$
-^nuterm::live@8 = 0$
-^nuterm::live@9 = 0$
-^nuterm::live@10 = 1$
+^Verilog::main\.\$live@0 = 0$
+^Verilog::main\.\$live@1 = 0$
+^Verilog::main\.\$live@2 = 0$
+^Verilog::main\.\$live@3 = 0$
+^Verilog::main\.\$live@4 = 0$
+^Verilog::main\.\$live@5 = 0$
+^Verilog::main\.\$live@6 = 0$
+^Verilog::main\.\$live@7 = 0$
+^Verilog::main\.\$live@8 = 0$
+^Verilog::main\.\$live@9 = 0$
+^Verilog::main\.\$live@10 = 1$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/nuterm/nuterm_main.cpp

@@ -282,6 +282,11 @@ int main(int argc, const char *argv[])
 
   std::cout << "Got " << tensors.size() << " transitions to rank\n";
 
+  if(tensors.empty())
+  {
+    return 0;
+  }
+
   const auto net = std::make_shared<RankingNet>(state_variables.size());
 
 #if 0