Skip to content

Commit 6e88f92

Browse files
authored
Merge pull request #6003 from padhi-aws-forks/smt2_implies_fix
[smt2_convt] Use `=>` in place of `implies`
2 parents d98b56b + 9ae905b commit 6e88f92

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -237,8 +237,8 @@ void smt2_convt::define_object_size(
237237
continue;
238238
}
239239

240-
out << "(assert (implies (= " <<
241-
"((_ extract " << h << " " << l << ") ";
240+
out << "(assert (=> (= "
241+
<< "((_ extract " << h << " " << l << ") ";
242242
convert_expr(ptr);
243243
out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
244244
<< "(= " << id << " (_ bv" << *object_size << " " << size_width

0 commit comments

Comments
 (0)