197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
|
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
|
+
-
+
|
optional< z3::expr > BuildZ3Op( Builder& b, const SLE& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs <= rhs; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const Assert& instr )
{
// TODO: refactor the return value here to be able to indicate failure versus "nothing to do"
auto cond = BuildZ3ExprFromValue( b, instr.cond() );
if( cond )
b.addAssertion( *cond, instr.cond().locationId() );
b.checkAssertion( *cond, instr.cond().locationId() );
return nullopt;
}
optional< z3::expr > BuildZ3Op( Builder& b, const Placeholder& instr )
{
const auto* expr = b.retrievePlaceholder( instr.name() );
if( expr )
|