From 94f995ee3784e1a94a484fd399be2be4793d4e41 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 9 Mar 2019 13:19:41 -0800 Subject: Fix signed $shift/$shiftx handling in write_smt2 Signed-off-by: Clifford Wolf --- backends/smt2/smt2.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a26bff57b..688535f33 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -416,6 +416,7 @@ struct Smt2Worker for (char ch : expr) { if (ch == 'A') processed_expr += get_bv(sig_a); else if (ch == 'B') processed_expr += get_bv(sig_b); + else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B")); else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; else processed_expr += ch; @@ -554,7 +555,7 @@ struct Smt2Worker if (cell->type.in("$shift", "$shiftx")) { if (cell->getParam("\\B_SIGNED").as_bool()) { - return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) " + return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) " "(bvlshr A B) (bvlshr A (bvneg B)))", GetSize(cell->getPort("\\B")), 0), 's'); } else { -- cgit v1.2.3