Fix 2's complement

This commit is contained in:
Leo Alt 2021-05-18 23:01:13 +02:00
parent 95f973e08a
commit 5c3b5f86f3

View File

@ -175,7 +175,7 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
sexpr += string("ite ") + sexpr += string("ite ") +
"(= ((_ extract " + pos + " " + pos + ")" + arg + ") #b0) " + "(= ((_ extract " + pos + " " + pos + ")" + arg + ") #b0) " +
nat + " " + nat + " " +
"(- (bvneg " + arg + "))"; "(- (bv2nat (bvneg " + arg + ")))";
} }
else if (_expr.name == "const_array") else if (_expr.name == "const_array")
{ {