mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fixed error check in read_interpolation_problem
This commit is contained in:
parent
d815af9f0f
commit
6e18f44d99
|
@ -617,7 +617,7 @@ extern "C" {
|
|||
}
|
||||
|
||||
for (unsigned j = 0; j < num - 1; j++)
|
||||
if (read_parents[j] == SHRT_MIN){
|
||||
if (read_parents[j] == SHRT_MAX){
|
||||
read_error << "formula " << j + 1 << ": unreferenced";
|
||||
goto fail;
|
||||
}
|
||||
|
@ -717,4 +717,4 @@ Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
|
|||
__in unsigned incremental,
|
||||
__in unsigned num_theory,
|
||||
__in_ecount(num_theory) Z3_ast *theory);
|
||||
#endif
|
||||
#endif
|
||||
|
|
Loading…
Reference in a new issue