59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
unordered_set< uint32_t > convertedBBIndices = m_convertedBBIndices;
auto savedBuilder = m_builder;
auto savedRemapper = m_remapper;
// Set a different assertion handler for the induction case: we want to just emit them as assumptions.
m_builder.setAssertionHandler( [&]( const z3::expr& expr, const z3::expr& exprToCheck, LocationId locationId )
{
m_builder.assume( expr );
return true;
} );
VerifyViz::Guard vvg( m_viz );
m_viz.beginLoopInduction();
|
>
>
|
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
unordered_set< uint32_t > convertedBBIndices = m_convertedBBIndices;
auto savedBuilder = m_builder;
auto savedRemapper = m_remapper;
// Set a different assertion handler for the induction case: we want to just emit them as assumptions.
m_builder.setAssertionHandler( [&]( const z3::expr& expr, const z3::expr& exprToCheck, LocationId locationId )
{
if( ms_TraceMode )
cout << "assuming " << exprToCheck << endl;
m_builder.assume( expr );
return true;
} );
VerifyViz::Guard vvg( m_viz );
m_viz.beginLoopInduction();
|
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
if( k == maxK )
m_builder.setAssertionHandler( origAssHandler );
else
{
m_builder.setAssertionHandler( [&]( const z3::expr& expr, const z3::expr& exprToCheck, LocationId locationId )
{
if( ms_TraceMode )
return true;
z3::expr_vector exprVec( GetZ3Context() );
exprVec.push_back( exprToCheck );
bool result = m_solver.check( exprVec ) == z3::check_result::unsat;
if( ( !result && ms_DumpSolverOnFailure ) || ( result && ms_DumpSolverOnSuccess ) )
cout << "Solver dump:\n" << m_solver << "check_unsat_ind: " << exprToCheck << endl << endl;
|
>
>
>
|
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
if( k == maxK )
m_builder.setAssertionHandler( origAssHandler );
else
{
m_builder.setAssertionHandler( [&]( const z3::expr& expr, const z3::expr& exprToCheck, LocationId locationId )
{
if( ms_TraceMode )
{
cout << "check_unsat " << exprToCheck << endl;
return true;
}
z3::expr_vector exprVec( GetZ3Context() );
exprVec.push_back( exprToCheck );
bool result = m_solver.check( exprVec ) == z3::check_result::unsat;
if( ( !result && ms_DumpSolverOnFailure ) || ( result && ms_DumpSolverOnSuccess ) )
cout << "Solver dump:\n" << m_solver << "check_unsat_ind: " << exprToCheck << endl << endl;
|