Commit be34030f authored by Henrich Lauko's avatar Henrich Lauko

mc: Fix tracing of assumes.

parent ddf75635
......@@ -38,8 +38,7 @@ namespace divine::mc
brick::smt::Context ctx;
smt::extract::SMTLib2 extract( this->heap(), ctx, "", false );
auto assume = extract.read( ta.ptr );
auto n = extract.convert( assume->binary.left );
trace( "ASSUME " + to_string( n ) );
trace( "ASSUME " + to_string( evaluate( extract, assume ) ) );
}
}
};
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment