File tree Expand file tree Collapse file tree 4 files changed +13
-10
lines changed
regression/cbmc/Failing_Assert1 Expand file tree Collapse file tree 4 files changed +13
-10
lines changed Original file line number Diff line number Diff line change 1
1
CORE
2
2
main.c
3
-
3
+ --verbosity 8
4
4
^EXIT=10$
5
5
^SIGNAL=0$
6
6
^VERIFICATION FAILED$
Original file line number Diff line number Diff line change @@ -134,9 +134,10 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
134
134
{
135
135
auto solver_stop = std::chrono::steady_clock::now ();
136
136
137
- status () << " Runtime decision procedure: "
138
- << std::chrono::duration<double >(solver_stop-solver_start).count ()
139
- << " s" << eom;
137
+ statistics ()
138
+ << " Runtime decision procedure: "
139
+ << std::chrono::duration<double >(solver_stop - solver_start).count ()
140
+ << " s" << eom;
140
141
}
141
142
142
143
// report
Original file line number Diff line number Diff line change @@ -61,9 +61,10 @@ decision_proceduret::resultt bmct::run_decision_procedure()
61
61
62
62
{
63
63
auto solver_stop = std::chrono::steady_clock::now ();
64
- status () << " Runtime decision procedure: "
65
- << std::chrono::duration<double >(solver_stop-solver_start).count ()
66
- << " s" << eom;
64
+ statistics ()
65
+ << " Runtime decision procedure: "
66
+ << std::chrono::duration<double >(solver_stop - solver_start).count ()
67
+ << " s" << eom;
67
68
}
68
69
69
70
return dec_result;
Original file line number Diff line number Diff line change @@ -263,9 +263,10 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
263
263
264
264
{
265
265
auto solver_stop=std::chrono::steady_clock::now ();
266
- status () << " Runtime decision procedure: "
267
- << std::chrono::duration<double >(solver_stop-solver_start).count ()
268
- << " s" << eom;
266
+ statistics ()
267
+ << " Runtime decision procedure: "
268
+ << std::chrono::duration<double >(solver_stop - solver_start).count ()
269
+ << " s" << eom;
269
270
}
270
271
271
272
return dec_result;
You can’t perform that action at this time.
0 commit comments