Skip to content

Commit e07ed1b

Browse files
committed
Fixed nondet returns in benchmark
Benchmark contained unused, nondet return values which caused an assertion violation in remove_returns.cpp.
1 parent 06942bb commit e07ed1b

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

regression/cegis/cegis_control_benchmark_03/safety_stability.c

+2-3
Original file line numberDiff line numberDiff line change
@@ -450,7 +450,7 @@ void assert_nonzero_controller(void) {
450450
__DSVERIFIER_assert(nonzero_coefficients > 0);
451451
}
452452

453-
int safety_stability(void) {
453+
void safety_stability(void) {
454454
#ifdef INTERVAL
455455
get_bounds(); //get interval bounds
456456
#endif
@@ -466,8 +466,6 @@ int safety_stability(void) {
466466
__CPROVER_array_copy(K_fxp_trace, K_fxp);
467467
//__CPROVER_assert(0 == 1, "");
468468
#endif
469-
470-
return 0;
471469
}
472470

473471
int main(void) {
@@ -484,4 +482,5 @@ int main(void) {
484482
#ifndef CPROVER
485483
}
486484
#endif
485+
return 0;
487486
}

regression/cegis/cegis_control_benchmark_04/safety_stability.c

+2-1
Original file line numberDiff line numberDiff line change
@@ -466,7 +466,7 @@ void assert_nonzero_controller(void) {
466466
__DSVERIFIER_assert(nonzero_coefficients > 0);
467467
}
468468

469-
int safety_stability(void) {
469+
void safety_stability(void) {
470470
#ifdef INTERVAL
471471
get_bounds(); //get interval bounds
472472
#endif
@@ -502,4 +502,5 @@ int main(void) {
502502
#ifndef CPROVER
503503
}
504504
#endif
505+
return 0;
505506
}

0 commit comments

Comments
 (0)