Merge remote-tracking branch 'origin/master' into xaig_dff

2 files changed, 23 insertions, 20 deletions

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index f617b7ec2..9e316a055 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -569,7 +569,7 @@ struct BtorWorker
 			int nid_init_val = -1;
 
 			if (!initval.is_fully_undef())
-				nid_init_val = get_sig_nid(initval);
+				nid_init_val = get_sig_nid(initval, -1, false, true);
 
 			int sid = get_bv_sid(GetSize(sig_q));
 			int nid = next_nid++;
@@ -681,7 +681,7 @@ struct BtorWorker
 				{
 					if (verbose)
 						btorf("; initval = %s\n", log_signal(firstword));
-					nid_init_val = get_sig_nid(firstword);
+					nid_init_val = get_sig_nid(firstword, -1, false, true);
 				}
 				else
 				{
@@ -693,8 +693,8 @@ struct BtorWorker
 						if (thisword.is_fully_undef())
 							continue;
 						Const thisaddr(i, abits);
-						int nid_thisword = get_sig_nid(thisword);
-						int nid_thisaddr = get_sig_nid(thisaddr);
+						int nid_thisword = get_sig_nid(thisword, -1, false, true);
+						int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true);
 						int last_nid_init_val = nid_init_val;
 						nid_init_val = next_nid++;
 						if (verbose)
@@ -792,7 +792,7 @@ struct BtorWorker
 		cell_recursion_guard.erase(cell);
 	}
 
-	int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
+	int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false)
 	{
 		int nid = -1;
 		sigmap.apply(sig);
@@ -823,7 +823,10 @@ struct BtorWorker
 				int sid = get_bv_sid(GetSize(sig));
 
 				int nid_input = next_nid++;
-				btorf("%d input %d\n", nid_input, sid);
+				if (is_init)
+					btorf("%d state %d\n", nid_input, sid);
+				else
+					btorf("%d input %d\n", nid_input, sid);
 
 				int nid_masked_input;
 				if (sig_mask_undef.is_fully_ones()) {
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 445a42e0d..3d6d3e1b3 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1256,7 +1256,7 @@ def smt_check_sat():
     return smt.check_sat()
 
 if tempind:
-    retstatus = False
+    retstatus = "FAILED"
     skip_counter = step_size
     for step in range(num_steps, -1, -1):
         if smt.forall:
@@ -1303,7 +1303,7 @@ if tempind:
 
         else:
             print_msg("Temporal induction successful.")
-            retstatus = True
+            retstatus = "PASSED"
             break
 
 elif covermode:
@@ -1321,7 +1321,7 @@ elif covermode:
     smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
 
     step = 0
-    retstatus = False
+    retstatus = "FAILED"
     found_failed_assert = False
 
     assert step_size == 1
@@ -1365,7 +1365,7 @@ elif covermode:
                 if smt_check_sat() == "unsat":
                     print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
                     found_failed_assert = True
-                    retstatus = False
+                    retstatus = "FAILED"
                     break
 
             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
@@ -1400,7 +1400,7 @@ elif covermode:
             break
 
         if "1" not in cover_mask:
-            retstatus = True
+            retstatus = "PASSED"
             break
 
         step += 1
@@ -1412,7 +1412,7 @@ elif covermode:
 
 else:  # not tempind, covermode
     step = 0
-    retstatus = True
+    retstatus = "PASSED"
     while step < num_steps:
         smt_state(step)
         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
@@ -1459,8 +1459,8 @@ else:  # not tempind, covermode
                     print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
 
                 if smt_check_sat() == "unsat":
-                    print("%s Warmup failed!" % smt.timestamp())
-                    retstatus = False
+                    print("%s Assumptions are unsatisfiable!" % smt.timestamp())
+                    retstatus = "PREUNSAT"
                     break
 
             if not final_only:
@@ -1487,13 +1487,13 @@ else:  # not tempind, covermode
                         print_msg("Re-solving with appended steps..")
                         if smt_check_sat() == "unsat":
                             print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
-                            retstatus = False
+                            retstatus = "FAILED"
                             break
                     print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)
                     write_trace(0, last_check_step+1+append_steps, '%')
-                    retstatus = False
+                    retstatus = "FAILED"
                     break
 
                 smt_pop()
@@ -1519,7 +1519,7 @@ else:  # not tempind, covermode
                         print_anyconsts(i)
                         print_failed_asserts(i, final=True)
                         write_trace(0, i+1, '%')
-                        retstatus = False
+                        retstatus = "FAILED"
                         break
 
                     smt_pop()
@@ -1534,7 +1534,7 @@ else:  # not tempind, covermode
             print_msg("Solving for step %d.." % (last_check_step))
             if smt_check_sat() != "sat":
                 print("%s No solution found!" % smt.timestamp())
-                retstatus = False
+                retstatus = "FAILED"
                 break
 
             elif dumpall:
@@ -1551,5 +1551,5 @@ else:  # not tempind, covermode
 smt.write("(exit)")
 smt.wait()
 
-print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)"))
-sys.exit(0 if retstatus else 1)
+print_msg("Status: %s" % retstatus)
+sys.exit(0 if retstatus == "PASSED" else 1)