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

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-11-01 11:40:58 +01:00
parent b4d82aa245
commit b6781c6f4b
1 changed files with 3 additions and 1 deletions

View File

@ -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');
}