From e8b04790cf20688b5ef829912fcf8afa6da3f8dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Oct 2014 09:43:55 -0700 Subject: [PATCH] fix build by disabling removed API call from interpolation sample Signed-off-by: Nikolaj Bjorner --- examples/interp/iz3.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp index 26f62976f..6d631ebc9 100755 --- a/examples/interp/iz3.cpp +++ b/examples/interp/iz3.cpp @@ -144,7 +144,7 @@ int main(int argc, const char **argv) { if(!incremental_mode){ /* In non-incremental mode, we just pass the constraints. */ - result = Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &model, 0, false, num_theory, theory); + result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &model, 0, false, num_theory, theory); } else { @@ -165,7 +165,7 @@ int main(int argc, const char **argv) { for(int i = 0; i < num; i++){ asserted[i] = constraints[i]; Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint - result = Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0); + result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0); if(result == Z3_L_FALSE){ for(unsigned j = 0; j < num-1; j++) /* Since we want the interpolant formulas to survive a "pop", we