Add support for signed $shift/$shiftx in smt2 back-end

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e2777ae0463a274bdea00c04c42d45662c3c9224..418f8d76651f3677dc3aad23fb346dd7b172e874 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -554,7 +554,9 @@ struct Smt2Worker
 
                        if (cell->type.in("$shift", "$shiftx")) {
                                if (cell->getParam("\\B_SIGNED").as_bool()) {
-                                       /* FIXME */
+                                       return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) "
+                                                       "(bvlshr A B) (bvlshr A (bvneg B)))",
+                                                       GetSize(cell->getPort("\\B")), 0), 's');
                                } else {
                                        return export_bvop(cell, "(bvlshr A B)", 's');
                                }