Build updates:

- upgrade version of libpoly needed
- only use yices2 if libpoly is available
- extra include for new version of z3

CMakeLists.txt

@@ -45,22 +45,24 @@ else()
   message(FATAL_ERROR "Could not the GMP number library (sudo apt-get install libgmp-dev)")
 endif()
 
-# Find Yices
-SET(YICES2_HOME CACHE STRING "Yices2 installation directory")
-find_package(Yices2 2.6.0)
-if (YICES2_FOUND)
-  add_definitions(-DWITH_YICES2)
-  include_directories(${YICES2_INCLUDE_DIR}) 
-endif()
-
 # Find LibPoly
 SET(LIBPOLY_HOME CACHE STRING "LibPoly installation directory")
-find_package(LibPoly 0.1.1)
+find_package(LibPoly 0.1.5)
 if (LIBPOLY_FOUND)
   add_definitions(-DWITH_LIBPOLY)
   include_directories(${LIBPOLY_INCLUDE_DIR})
 endif()
 
+# Find Yices if LibPoly is there
+if (LIBPOLY_FOUND)
+  SET(YICES2_HOME CACHE STRING "Yices2 installation directory")
+  find_package(Yices2 2.6.0)
+  if (YICES2_FOUND)
+    add_definitions(-DWITH_YICES2)
+    include_directories(${YICES2_INCLUDE_DIR}) 
+  endif()
+endif()
+
 # Find MathSAT5
 SET(MATHSAT5_HOME CACHE STRING "MathSAT5 installation directory")
 find_package(MathSAT5 5.3.3)

src/smt/z3/z3_internal.cpp

@@ -20,6 +20,7 @@
 
 #include "smt/z3/z3_internal.h"
 #include "z3_common.h"
+#include "z3_interp.h"
 #include "utils/trace.h"
 #include "expr/gc_relocator.h"
 #include "utils/output.h"
@@ -478,9 +479,6 @@ expr::term_ref z3_internal::mk_term(Z3_decl_kind kind, const std::vector<expr::t
   case Z3_OP_OEQ:
     assert(false);
     break;
-  case Z3_OP_INTERP:
-    assert(false);
-    break;
 
     // Arithmetic
   case Z3_OP_ANUM: