62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
-
+
|
)
);
if( !result )
return true;
auto&& [type, val, locId] = *result;
auto paramVal = BuildComputedValue( type, VarAddr( varId++, type ), Load( type ) );
auto paramVal = BuildComputedValue( type, VarAddr( varId++, type, locId ), Load( type, locId ) );
if( auto zv = BuildZ3ExprFromValue( cb, paramVal ) )
{
ForEachPredicate( cb, type, zv->expr, [&]( auto&& z3expr, auto locId )
{
DiagnosticsContext dc( fVal->locationId(), "At this call." );
b.checkAssertion( z3expr, locId );
|