From b6781c6f4ba20ba14d1649a993fc09691921de2b Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 1 Nov 2018 11:40:58 +0100
Subject: [PATCH] Add support for signed $shift/$shiftx in smt2 back-end

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 backends/smt2/smt2.cc | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e2777ae04..418f8d766 100644
--- 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');
 				}
-- 
2.30.2