diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 4f6845849..65729efa9 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -100,7 +100,7 @@ with open(args[0], "r") as f:
         smt.write(line)
 
 
-def write_vcd_model():
+def write_vcd_model(steps):
     print("%s Writing model to VCD file." % smt.timestamp())
 
     vcd = mkvcd(open(vcdfile, "w"))
@@ -108,12 +108,12 @@ def write_vcd_model():
         width = len(smt.get_net_bin(topmod, netname, "s0"))
         vcd.add_net(netname, width)
 
-    for i in range(step+1):
+    for i in range(steps):
         vcd.set_time(i)
         for netname in debug_nets:
             vcd.set_net(netname, smt.get_net_bin(topmod, netname, "s%d" % i))
 
-    vcd.set_time(step+1)
+    vcd.set_time(steps)
 
 
 if tempind:
@@ -138,7 +138,7 @@ if tempind:
             if step == 0:
                 print("%s temporal induction failed!" % smt.timestamp())
                 if vcdfile is not None:
-                    write_vcd_model()
+                    write_vcd_model(num_steps+1)
 
         else:
             print("%s PASSED." % smt.timestamp())
@@ -172,7 +172,7 @@ else: # not tempind
         if smt.check_sat() == "sat":
             print("%s BMC failed!" % smt.timestamp())
             if vcdfile is not None:
-                write_vcd_model()
+                write_vcd_model(steps+1)
             break
 
         else: # unsat
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index acaf8f30f..799efa88c 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -193,10 +193,9 @@ class smtio:
         return worker(stmt)[0]
 
     def bv2hex(self, v):
-        if v == "true": return "1"
-        if v == "false": return "0"
         h = ""
-        while len(v) > 2:
+        v = bv2bin(v)
+        while len(v) > 0:
             d = 0
             if len(v) > 0 and v[-1] == "1": d += 1
             if len(v) > 1 and v[-2] == "1": d += 2
@@ -210,7 +209,29 @@ class smtio:
     def bv2bin(self, v):
         if v == "true": return "1"
         if v == "false": return "0"
-        return v[2:]
+        if v.startswith("#b"):
+            return v[2:]
+        if v.startswith("#x"):
+            digits = []
+            for d in v[2:]:
+                if d == "0": digits.append("0000")
+                if d == "1": digits.append("0001")
+                if d == "2": digits.append("0010")
+                if d == "3": digits.append("0011")
+                if d == "4": digits.append("0100")
+                if d == "5": digits.append("0101")
+                if d == "6": digits.append("0110")
+                if d == "7": digits.append("0111")
+                if d == "8": digits.append("1000")
+                if d == "9": digits.append("1001")
+                if d in ("a", "A"): digits.append("1010")
+                if d in ("b", "B"): digits.append("1011")
+                if d in ("c", "C"): digits.append("1100")
+                if d in ("d", "D"): digits.append("1101")
+                if d in ("e", "E"): digits.append("1110")
+                if d in ("f", "F"): digits.append("1111")
+            return "".join(digits)
+        assert False
 
     def get(self, expr):
         self.write("(get-value (%s))" % (expr))