diff --git a/backends/smt2/example.v b/backends/smt2/example.v
new file mode 100644
index 000000000..b195266eb
--- /dev/null
+++ b/backends/smt2/example.v
@@ -0,0 +1,11 @@
+module main(input clk);
+	reg [3:0] counter = 0;
+	always @(posedge clk) begin
+		if (counter == 10)
+			counter <= 0;
+		else
+			counter <= counter + 1;
+	end
+	assert property (counter != 15);
+	// assert property (counter <= 10);
+endmodule
diff --git a/backends/smt2/example.ys b/backends/smt2/example.ys
new file mode 100644
index 000000000..6fccb344f
--- /dev/null
+++ b/backends/smt2/example.ys
@@ -0,0 +1,3 @@
+read_verilog -formal example.v
+hierarchy; proc; opt; memory -nordff -nomap; opt -fast
+write_smt2 -bv -mem -wires example.smt2
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
new file mode 100644
index 000000000..283d12319
--- /dev/null
+++ b/backends/smt2/smtbmc.py
@@ -0,0 +1,110 @@
+#!/usr/bin/env python3
+
+import os, sys, getopt, re
+from smtio import smtio, smtopts, mkvcd
+
+steps = 20
+vcdfile = None
+tempind = False
+topmod = "main"
+so = smtopts()
+
+def usage():
+    print("""
+python3 smtbmc.py [options] <yosys_smt2_output>
+
+    -t <steps>
+        default: 20
+
+    -c <vcd_filename>
+        write counter-example to this VCD file
+
+    -i
+        instead of BMC run temporal induction
+
+    -m <module_name>
+        name of the top module, default: main
+""" + so.helpmsg())
+    sys.exit(1)
+
+try:
+    opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:c:im:")
+except:
+    usage()
+
+for o, a in opts:
+    if o == "-t":
+        steps = int(a)
+    elif o == "-c":
+        vcdfile = a
+    elif o == "-i":
+        tempind = True
+        print("FIXME: temporal induction not yet implemented!")
+        assert False
+    elif so.handle(o, a):
+        pass
+    else:
+        usage()
+
+if len(args) != 1:
+    usage()
+
+smt = smtio(opts=so)
+
+print("Solver: %s" % so.solver)
+smt.setup("QF_AUFBV")
+
+debug_nets = set()
+debug_nets_re = re.compile(r"^; yosys-smt2-(input|output|register|wire) (\S+) (\d+)")
+
+with open(args[0], "r") as f:
+    for line in f:
+        match = debug_nets_re.match(line)
+        if match:
+            debug_nets.add(match.group(2))
+        smt.write(line)
+
+def write_vcd_model():
+    print("%s Writing model to VCD file." % smt.timestamp())
+
+    vcd = mkvcd(open(vcdfile, "w"))
+    for netname in sorted(debug_nets):
+        width = len(smt.get_net_bin("main", netname, "s0"))
+        vcd.add_net(netname, width)
+
+    for i in range(step+1):
+        vcd.set_time(i)
+        for netname in debug_nets:
+            vcd.set_net(netname, smt.get_net_bin("main", netname, "s%d" % i))
+
+    vcd.set_time(step+1)
+
+for step in range(steps):
+    smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
+    smt.write("(assert (%s_u s0))" % (topmod))
+
+    if step == 0:
+        smt.write("(assert (%s_i s0))" % (topmod))
+
+    else:
+        smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
+
+    print("%s Checking sequence of length %d.." % (smt.timestamp(), step))
+    smt.write("(push 1)")
+
+    smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
+
+    if smt.check_sat() == "sat":
+        print("%s BMC failed!" % smt.timestamp())
+        if vcdfile is not None:
+            write_vcd_model()
+        break
+
+    else: # unsat
+        smt.write("(pop 1)")
+        smt.write("(assert (%s_a s%d))" % (topmod, step))
+
+print("%s Done." % smt.timestamp())
+smt.write("(exit)")
+smt.wait()
+
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
new file mode 100644
index 000000000..774984f2d
--- /dev/null
+++ b/backends/smt2/smtio.py
@@ -0,0 +1,285 @@
+#!/usr/bin/env python3
+
+import sys
+import subprocess
+from select import select
+from time import time
+
+class smtio:
+    def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
+        if opts is not None:
+            self.solver = opts.solver
+            self.debug_print = opts.debug_print
+            self.debug_file = opts.debug_file
+            self.timeinfo = opts.timeinfo
+
+        else:
+            self.solver = "z3"
+            self.debug_print = False
+            self.debug_file = None
+            self.timeinfo = True
+
+        if solver is not None:
+            self.solver = solver
+
+        if debug_print is not None:
+            self.debug_print = debug_print
+
+        if debug_file is not None:
+            self.debug_file = debug_file
+
+        if timeinfo is not None:
+            self.timeinfo = timeinfo
+
+        if self.solver == "yices":
+            popen_vargs = ['yices-smt2', '--incremental']
+
+        if self.solver == "z3":
+            popen_vargs = ['z3', '-smt2', '-in']
+
+        if self.solver == "cvc4":
+            popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
+
+        if self.solver == "mathsat":
+            popen_vargs = ['mathsat']
+
+        self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+        self.start_time = time()
+
+    def setup(self, logic="ALL", info=None):
+        self.write("(set-logic %s)" % logic)
+        if info is not None:
+            self.write("(set-info :source |%s|)" % info)
+        self.write("(set-info :smt-lib-version 2.5)")
+        self.write("(set-info :category \"industrial\")")
+
+    def timestamp(self):
+        secs = int(time() - self.start_time)
+        return "+ %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+
+    def write(self, stmt):
+        stmt = stmt.strip()
+        if self.debug_print:
+            print("> %s" % stmt)
+        if self.debug_file:
+            print(stmt, file=self.debug_file)
+            self.debug_file.flush()
+        self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+        self.p.stdin.flush()
+
+    def read(self):
+        stmt = []
+        count_brackets = 0
+
+        while True:
+            line = self.p.stdout.readline().decode("ascii").strip()
+            count_brackets += line.count("(")
+            count_brackets -= line.count(")")
+            stmt.append(line)
+            if self.debug_print:
+                print("< %s" % line)
+            if count_brackets == 0:
+                break
+            if not self.p.poll():
+                print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
+                sys.exit(1)
+
+        stmt = "".join(stmt)
+        if stmt.startswith("(error"):
+            print("SMT Solver Error: %s" % stmt, file=sys.stderr)
+            sys.exit(1)
+
+        return stmt
+
+    def check_sat(self):
+        if self.debug_print:
+            print("> (check-sat)")
+        if self.debug_file:
+            print("; running check-sat..", file=self.debug_file)
+            self.debug_file.flush()
+
+        self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
+        self.p.stdin.flush()
+
+        if self.timeinfo:
+            i = 0
+            s = "/-\|"
+
+            count = 0
+            num_bs = 0
+            while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+                count += 1
+
+                if count < 25:
+                    continue
+
+                if count % 10 == 0 or count == 25:
+                    secs = count // 10
+
+                    if secs < 60:
+                        m = "(%d seconds)" % secs
+                    elif secs < 60*60:
+                        m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
+                    else:
+                        m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+
+                    print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
+                    num_bs = len(m) + 3
+
+                else:
+                    print("\b" + s[i], end="", file=sys.stderr)
+
+                sys.stderr.flush()
+                i = (i + 1) % len(s)
+
+            if num_bs != 0:
+                print("\b \b" * num_bs, end="", file=sys.stderr)
+                sys.stderr.flush()
+
+        result = self.read()
+        if self.debug_file:
+            print("(set-info :status %s)" % result, file=self.debug_file)
+            print("(check-sat)", file=self.debug_file)
+            self.debug_file.flush()
+        return result
+
+    def parse(self, stmt):
+        def worker(stmt):
+            if stmt[0] == '(':
+                expr = []
+                cursor = 1
+                while stmt[cursor] != ')':
+                    el, le = worker(stmt[cursor:])
+                    expr.append(el)
+                    cursor += le
+                return expr, cursor+1
+
+            if stmt[0] == '|':
+                expr = "|"
+                cursor = 1
+                while stmt[cursor] != '|':
+                    expr += stmt[cursor]
+                    cursor += 1
+                expr += "|"
+                return expr, cursor+1
+
+            if stmt[0] in [" ", "\t", "\r", "\n"]:
+                el, le = worker(stmt[1:])
+                return el, le+1
+
+            expr = ""
+            cursor = 0
+            while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
+                expr += stmt[cursor]
+                cursor += 1
+            return expr, cursor
+        return worker(stmt)[0]
+
+    def bv2hex(self, v):
+        if v == "true": return "1"
+        if v == "false": return "0"
+        h = ""
+        while len(v) > 2:
+            d = 0
+            if len(v) > 0 and v[-1] == "1": d += 1
+            if len(v) > 1 and v[-2] == "1": d += 2
+            if len(v) > 2 and v[-3] == "1": d += 4
+            if len(v) > 3 and v[-4] == "1": d += 8
+            h = hex(d)[2:] + h
+            if len(v) < 4: break
+            v = v[:-4]
+        return h
+
+    def bv2bin(self, v):
+        if v == "true": return "1"
+        if v == "false": return "0"
+        return v[2:]
+
+    def get(self, expr):
+        self.write("(get-value (%s))" % (expr))
+        return self.parse(self.read())[0][1]
+
+    def get_net(self, mod_name, net_name, state_name):
+        return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
+
+    def get_net_bool(self, mod_name, net_name, state_name):
+        v = self.get_net(mod_name, net_name, state_name)
+        assert v in ["true", "false"]
+        return 1 if v == "true" else 0
+
+    def get_net_hex(self, mod_name, net_name, state_name):
+        return self.bv2hex(self.get_net(mod_name, net_name, state_name))
+
+    def get_net_bin(self, mod_name, net_name, state_name):
+        return self.bv2bin(self.get_net(mod_name, net_name, state_name))
+
+    def wait(self):
+        self.p.wait()
+
+
+class smtopts:
+    def __init__(self):
+        self.optstr = "s:d:vp"
+        self.solver = "z3"
+        self.debug_print = False
+        self.debug_file = None
+        self.timeinfo = True
+
+    def handle(self, o, a):
+        if o == "-s":
+            self.solver = a
+        elif o == "-v":
+            self.debug_print = True
+        elif o == "-p":
+            self.timeinfo = True
+        elif o == "-d":
+            self.debug_file = open(a, "w")
+        else:
+            return False
+        return True
+
+    def helpmsg(self):
+        return """
+    -s <solver>
+        set SMT solver: z3, cvc4, yices, mathsat
+        default: z3
+
+    -v
+        enable debug output
+
+    -p
+        disable timer display during solving
+
+    -d <filename>
+        write smt2 statements to file
+"""
+
+
+class mkvcd:
+    def __init__(self, f):
+        self.f = f
+        self.t = -1
+        self.nets = dict()
+
+    def add_net(self, name, width):
+        assert self.t == -1
+        key = "n%d" % len(self.nets)
+        self.nets[name] = (key, width)
+
+    def set_net(self, name, bits):
+        assert name in self.nets
+        assert self.t >= 0
+        print("b%s %s" % (bits, self.nets[name][0]), file=self.f)
+
+    def set_time(self, t):
+        assert t >= self.t
+        if t != self.t:
+            if self.t == -1:
+                for name in sorted(self.nets):
+                    key, width = self.nets[name]
+                    print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
+                print("$enddefinitions $end", file=self.f)
+            self.t = t
+            assert self.t >= 0
+            print("#%d" % self.t, file=self.f)
+