Skip to content

Commit 9ae905b

Browse files
committed
[smt2_convt] Use => in place of implies
Both CVC4 and Z3 reject `implies` keyword: - CVC4 rejects it even with `ALL` logic - Z3 rejects it when QF_AUFBV is supplied
1 parent 3cd4054 commit 9ae905b

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)