Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)

Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

20 files changed, 564 insertions, 44 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 65ccabd89..9753f86a7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -202,6 +202,8 @@ libcvc4_add_sources(
   smt/logic_exception.h
   smt/logic_request.cpp
   smt/logic_request.h
+  smt/interpolation_solver.cpp
+  smt/interpolation_solver.h
   smt/managed_ostreams.cpp
   smt/managed_ostreams.h
   smt/model.cpp
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
new file mode 100644
index 000000000..d2193d226
--- /dev/null
+++ b/src/smt/interpolation_solver.cpp
@@ -0,0 +1,142 @@
+/*********************                                                        */
+/*! \file interpolation_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Ying Sheng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for interpolation queries
+ **/
+
+#include "smt/interpolation_solver.h"
+
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_interpol.h"
+#include "theory/smt_engine_subsolver.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent)
+{
+}
+
+InterpolationSolver::~InterpolationSolver() {}
+
+bool InterpolationSolver::getInterpol(const Node& conj,
+                                      const TypeNode& grammarType,
+                                      Node& interpol)
+{
+  if (options::produceInterpols() == options::ProduceInterpols::NONE)
+  {
+    const char* msg =
+        "Cannot get interpolation when produce-interpol options is off.";
+    throw ModalException(msg);
+  }
+  Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj
+                          << std::endl;
+  std::vector<Expr> easserts = d_parent->getExpandedAssertions();
+  std::vector<Node> axioms;
+  for (unsigned i = 0, size = easserts.size(); i < size; i++)
+  {
+    axioms.push_back(Node::fromExpr(easserts[i]));
+  }
+  // must expand definitions
+  Node conjn = d_parent->expandDefinitions(conj);
+  std::string name("A");
+
+  quantifiers::SygusInterpol interpolSolver;
+  if (interpolSolver.SolveInterpolation(
+          name, axioms, conjn, grammarType, interpol))
+  {
+    if (options::checkInterpols())
+    {
+      checkInterpol(interpol.toExpr(), easserts, conj);
+    }
+    return true;
+  }
+  return false;
+}
+
+bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol)
+{
+  TypeNode grammarType;
+  return getInterpol(conj, grammarType, interpol);
+}
+
+void InterpolationSolver::checkInterpol(Expr interpol,
+                                        const std::vector<Expr>& easserts,
+                                        const Node& conj)
+{
+  Assert(interpol.getType().isBoolean());
+  Trace("check-interpol") << "SmtEngine::checkInterpol: get expanded assertions"
+                          << std::endl;
+
+  // two checks: first, axioms imply interpol, second, interpol implies conj.
+  for (unsigned j = 0; j < 2; j++)
+  {
+    if (j == 1)
+    {
+      Trace("check-interpol") << "SmtEngine::checkInterpol: conjecture is "
+                              << conj.toExpr() << std::endl;
+    }
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": make new SMT engine" << std::endl;
+    // Start new SMT engine to check solution
+    std::unique_ptr<SmtEngine> itpChecker;
+    initializeSubsolver(itpChecker);
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": asserting formulas" << std::endl;
+    if (j == 0)
+    {
+      for (const Expr& e : easserts)
+      {
+        itpChecker->assertFormula(e);
+      }
+      Expr negitp = interpol.notExpr();
+      itpChecker->assertFormula(negitp);
+    }
+    else
+    {
+      itpChecker->assertFormula(interpol);
+      Assert(!conj.isNull());
+      itpChecker->assertFormula(conj.toExpr().notExpr());
+    }
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": check the assertions" << std::endl;
+    Result r = itpChecker->checkSat();
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": result is " << r << std::endl;
+    std::stringstream serr;
+    if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+    {
+      if (j == 0)
+      {
+        serr << "SmtEngine::checkInterpol(): negated produced solution cannot "
+                "be shown "
+                "satisfiable with assertions, result was "
+             << r;
+      }
+      else
+      {
+        serr
+            << "SmtEngine::checkInterpol(): negated conjecture cannot be shown "
+               "satisfiable with produced solution, result was "
+            << r;
+      }
+      InternalError() << serr.str();
+    }
+  }
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
new file mode 100644
index 000000000..8e6d2cd14
--- /dev/null
+++ b/src/smt/interpolation_solver.h
@@ -0,0 +1,86 @@
+/*********************                                                        */
+/*! \file interpolation_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Ying Sheng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for interpolation queries
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__INTERPOLATION_SOLVER_H
+#define CVC4__SMT__INTERPOLATION_SOLVER_H
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/**
+ * A solver for interpolation queries.
+ *
+ * This class is responsible for responding to get-interpol commands. It spawns
+ * a subsolver SmtEngine for a sygus conjecture that captures the interpolation
+ * query, and implements supporting utility methods such as checkInterpol.
+ */
+class InterpolationSolver
+{
+ public:
+  InterpolationSolver(SmtEngine* parent);
+  ~InterpolationSolver();
+
+  /**
+   * This method asks this SMT engine to find an interpolant with respect to
+   * the current assertion stack (call it A) and the conjecture (call it B). If
+   * this method returns true, then interpolant is set to a formula I such that
+   * A ^ ~I and I ^ ~B are both unsatisfiable.
+   *
+   * @param conj The conjecture of the interpolation problem.
+   * @param grammarType A sygus datatype type that encodes the syntax
+   * restrictions on the shape of possible solutions.
+   * @param interpol This argument is updated to contain the solution to the
+   * interpolation problem.
+   *
+   * This method invokes a separate copy of the SMT engine for solving the
+   * corresponding sygus problem for generating such a solution.
+   */
+  bool getInterpol(const Node& conj,
+                   const TypeNode& grammarType,
+                   Node& interpol);
+
+  /**
+   * Same as above, but without user-provided grammar restrictions. A default
+   * grammar is chosen internally using the sygus grammar constructor utility.
+   */
+  bool getInterpol(const Node& conj, Node& interpol);
+
+  /**
+   * Check that a solution to an interpolation problem is indeed a solution.
+   *
+   * The check is made by determining that the assertions imply the solution of
+   * the interpolation problem (interpol), and the solution implies the goal
+   * (conj). If these criteria are not met, an internal error is thrown.
+   */
+  void checkInterpol(Expr interpol,
+                     const std::vector<Expr>& easserts,
+                     const Node& conj);
+
+ private:
+  /** The parent SMT engine */
+  SmtEngine* d_parent;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7f824bff3..d271ca05d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -75,6 +75,7 @@
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
 #include "smt/expr_names.h"
+#include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
 #include "smt/logic_request.h"
 #include "smt/model_blocker.h"
@@ -134,6 +135,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_definedFunctions(nullptr),
       d_sygusSolver(nullptr),
       d_abductSolver(nullptr),
+      d_interpolSolver(nullptr),
       d_quantElimSolver(nullptr),
       d_assignments(nullptr),
       d_logic(),
@@ -299,6 +301,10 @@ void SmtEngine::finishInit()
   {
     d_abductSolver.reset(new AbductionSolver(this));
   }
+  if (options::produceInterpols() != options::ProduceInterpols::NONE)
+  {
+    d_interpolSolver.reset(new InterpolationSolver(this));
+  }
 
   d_pp->finishInit();
 
@@ -1755,12 +1761,6 @@ void SmtEngine::checkModel(bool hardFailure) {
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
 }
 
-void SmtEngine::checkInterpol(Expr interpol,
-                              const std::vector<Expr>& easserts,
-                              const Node& conj)
-{
-}
-
 // TODO(#1108): Simplify the error reporting of this method.
 UnsatCore SmtEngine::getUnsatCore() {
   Trace("smt") << "SMT getUnsatCore()" << endl;
@@ -1818,7 +1818,11 @@ bool SmtEngine::getInterpol(const Node& conj,
                             const TypeNode& grammarType,
                             Node& interpol)
 {
-  return false;
+  bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol);
+  // notify the state of whether the get-interpol call was successfuly, which
+  // impacts the SMT mode.
+  d_state->notifyGetInterpol(success);
+  return success;
 }
 
 bool SmtEngine::getInterpol(const Node& conj, Node& interpol)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e95e36c3d..eec17a5f8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -105,6 +105,7 @@ class Preprocessor;
 class SmtSolver;
 class SygusSolver;
 class AbductionSolver;
+class InterpolationSolver;
 class QuantElimSolver;
 /**
  * Representation of a defined function.  We keep these around in
@@ -1101,6 +1102,8 @@ class CVC4_PUBLIC SmtEngine
 
   /** The solver for abduction queries */
   std::unique_ptr<smt::AbductionSolver> d_abductSolver;
+  /** The solver for interpolation queries */
+  std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
   /** The solver for quantifier elimination queries */
   std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
   /**
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 07f1d3321..4f3782e2a 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -122,6 +122,20 @@ void SmtEngineState::notifyGetAbduct(bool success)
   }
 }
 
+void SmtEngineState::notifyGetInterpol(bool success)
+{
+  if (success)
+  {
+    // successfully generated an interpolant, update to interpol state
+    d_smtMode = SmtMode::INTERPOL;
+  }
+  else
+  {
+    // failed, we revert to the assert state
+    d_smtMode = SmtMode::ASSERT;
+  }
+}
+
 void SmtEngineState::setup()
 {
   // push a context
diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h
index efb86ca88..1a2ae7ee8 100644
--- a/src/smt/smt_engine_state.h
+++ b/src/smt/smt_engine_state.h
@@ -96,6 +96,18 @@ class SmtEngineState
    */
   void notifyGetAbduct(bool success);
   /**
+   * Notify that we finished an interpolation query, where success is whether
+   * the command was successful. This is managed independently of the above
+   * calls for notifying check-sat. In other words, if a get-interpol command
+   * is issued to an SmtEngine, it may use a satisfiability call (if desired)
+   * to solve the interpolation query. This method is called *in addition* to
+   * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
+   * In particular, it is called after these two methods are completed.
+   * This overwrites the SMT mode to the "INTERPOL" mode if the call to
+   * interpolation was successful.
+   */
+  void notifyGetInterpol(bool success);
+  /**
    * Setup the context, which makes a single push to maintain a global
    * context around everything.
    */
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index c2ca83e41..4d18c850b 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/rewriter.h"
+#include "theory/smt_engine_subsolver.h"
 
 namespace CVC4 {
 namespace theory {
@@ -30,8 +31,6 @@ namespace quantifiers {
 
 SygusInterpol::SygusInterpol() {}
 
-SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {}
-
 void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
                                    const Node& conj)
 {
@@ -75,6 +74,9 @@ void SygusInterpol::createVariables(bool needsShared)
     Node var = nm->mkBoundVar(tn);
     d_vars.push_back(var);
     Node vlv = nm->mkBoundVar(ss.str(), tn);
+    // set that this variable encodes the term s
+    SygusVarToTermAttribute sta;
+    vlv.setAttribute(sta, s);
     d_vlvs.push_back(vlv);
     if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end())
     {
@@ -266,7 +268,7 @@ void SygusInterpol::mkSygusConjecture(Node itp,
   Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
 }
 
-bool SygusInterpol::findInterpol(Expr& interpol, Node itp)
+bool SygusInterpol::findInterpol(Node& interpol, Node itp)
 {
   // get the synthesis solution
   std::map<Node, Node> sols;
@@ -283,31 +285,31 @@ bool SygusInterpol::findInterpol(Expr& interpol, Node itp)
   }
   Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is "
                           << its->second << std::endl;
-  Node interpoln = its->second;
+  interpol = its->second;
   // replace back the created variables to original symbols.
-  Node interpoln_reduced;
-  if (interpoln.getKind() == kind::LAMBDA)
+  if (interpol.getKind() == kind::LAMBDA)
   {
-    interpoln_reduced = interpoln[1];
+    interpol = interpol[1];
   }
-  else
+
+  // get the grammar type for the interpolant
+  Node igdtbv = itp.getAttribute(SygusSynthFunVarListAttribute());
+  Assert(!igdtbv.isNull());
+  Assert(igdtbv.getKind() == kind::BOUND_VAR_LIST);
+  // convert back to original
+  // must replace formal arguments of itp with the free variables in the
+  // input problem that they correspond to.
+  std::vector<Node> vars;
+  std::vector<Node> syms;
+  SygusVarToTermAttribute sta;
+  for (const Node& bv : igdtbv)
   {
-    interpoln_reduced = interpoln;
+    vars.push_back(bv);
+    syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
   }
-  if (interpoln.getNumChildren() != 0 && interpoln[0].getNumChildren() != 0)
-  {
-    std::vector<Node> formals;
-    for (const Node& n : interpoln[0])
-    {
-      formals.push_back(n);
-    }
-    interpoln_reduced = interpoln_reduced.substitute(formals.begin(),
-                                                     formals.end(),
-                                                     d_symSetShared.begin(),
-                                                     d_symSetShared.end());
-  }
-  // convert to expression
-  interpol = interpoln_reduced.toExpr();
+  interpol =
+      interpol.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
+
   return true;
 }
 
@@ -315,14 +317,11 @@ bool SygusInterpol::SolveInterpolation(const std::string& name,
                                        const std::vector<Node>& axioms,
                                        const Node& conj,
                                        const TypeNode& itpGType,
-                                       Expr& interpol)
+                                       Node& interpol)
 {
-  NodeManager* nm = NodeManager::currentNM();
-  // we generate a new smt engine to do the interpolation query
-  d_subSolver.reset(new SmtEngine(nm->toExprManager()));
-  d_subSolver->setIsInternalSubsolver();
+  initializeSubsolver(d_subSolver);
   // get the logic
-  LogicInfo l = d_logic.getUnlockedCopy();
+  LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy();
   // enable everything needed for sygus
   l.enableSygus();
   d_subSolver->setLogic(l);
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 0fe66694f..4abe94f15 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -46,8 +46,6 @@ class SygusInterpol
  public:
   SygusInterpol();
 
-  SygusInterpol(LogicInfo logic);
-
   /**
    * Returns the sygus conjecture in interpol corresponding to the interpolation
    * problem for input problem (F above) given by axioms (Fa above), and conj
@@ -65,7 +63,7 @@ class SygusInterpol
                           const std::vector<Node>& axioms,
                           const Node& conj,
                           const TypeNode& itpGType,
-                          Expr& interpol);
+                          Node& interpol);
 
  private:
   /**
@@ -158,7 +156,7 @@ class SygusInterpol
    * @param interpol the solution to the sygus conjecture.
    * @param itp the interpolation predicate.
    */
-  bool findInterpol(Expr& interpol, Node itp);
+  bool findInterpol(Node& interpol, Node itp);
 
   /** The SMT engine subSolver
    *
@@ -179,10 +177,6 @@ class SygusInterpol
   std::unique_ptr<SmtEngine> d_subSolver;
 
   /**
-   * The logic for the local copy of SMT engine (d_subSolver).
-   */
-  LogicInfo d_logic;
-  /**
    * symbols from axioms and conjecture.
    */
   std::vector<Node> d_syms;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d784a1ced..ef0981372 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1943,6 +1943,14 @@ set(regress_1_tests
   regress1/sygus/inv-example.sy
   regress1/sygus/inv-missed-sol-true.sy
   regress1/sygus/inv-unused.sy
+  regress1/sygus/interpol1.smt2
+  regress1/sygus/interpol2.smt2
+  regress1/sygus/interpol3.smt2
+  regress1/sygus/interpol_arr1.smt2
+  regress1/sygus/interpol_arr2.smt2
+  regress1/sygus/interpol_cosa_1.smt2
+  regress1/sygus/interpol_from_pono_1.smt2
+  regress1/sygus/interpol_from_pono_2.smt2
   regress1/sygus/issue2914.sy
   regress1/sygus/issue2935.sy
   regress1/sygus/issue3199.smt2
diff --git a/test/regress/regress1/sygus/interpol1.smt2 b/test/regress/regress1/sygus/interpol1.smt2
new file mode 100644
index 000000000..58ef5420f
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol1.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic NIA)
+(declare-fun x ( ) Int)
+(declare-fun y ( ) Int)
+(declare-fun z ( ) Int)
+(assert (= (* 2 x) y))
+(get-interpol A (distinct (+ (* 2 z) 1) y)
+
+; the grammar for the interpol-to-synthesize
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int 
+(y (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2))
+)
+
+)
diff --git a/test/regress/regress1/sygus/interpol2.smt2 b/test/regress/regress1/sygus/interpol2.smt2
new file mode 100644
index 000000000..c6876ee15
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol2.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic QF_UFLIA)
+
+; Let A1,...,An be formulas (called assumptions)
+; Let C be a formula (called a conjecture)
+; An interpolant of {A1,...,An} and G is any formula B such that:
+; - A1,...,An |- B
+; - B |- C
+; - B has only variables that occur both in {A_1,...,A_n} and B.
+
+;The variables used are n,m,x,y, all integers.
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+;The assumptions are:
+; (*) 1 <= n <= x <= n+5
+; (*) 1 <= y <= m
+(define-fun A1 () Bool (<= 1 n))
+(define-fun A2 () Bool (<= n x))
+(define-fun A3 () Bool (<= x (+ n 5)))
+(define-fun A4 () Bool (<= 1 y))
+(define-fun A5 () Bool (<= y m))
+(assert (and A1 A2 A3 A4 A5))
+
+;The conjuecture is: 2 <= x+y
+(get-interpol A (<= 2 (+ x y)))
diff --git a/test/regress/regress1/sygus/interpol3.smt2 b/test/regress/regress1/sygus/interpol3.smt2
new file mode 100644
index 000000000..8681acf3a
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol3.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --produce-interpols=default --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic LIA)
+(declare-fun a () Int)
+(assert (> a 1))
+(get-interpol A (> a 0))
diff --git a/test/regress/regress1/sygus/interpol_arr1.smt2 b/test/regress/regress1/sygus/interpol_arr1.smt2
new file mode 100644
index 000000000..16190f877
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_arr1.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a () (Array (_ BitVec 4) (_ BitVec 4)))
+(declare-fun y () (_ BitVec 4))
+(assert (= (select a y) (_ bv0 4)))
+(get-interpol A (distinct (select a y) (_ bv1 4)))
diff --git a/test/regress/regress1/sygus/interpol_arr2.smt2 b/test/regress/regress1/sygus/interpol_arr2.smt2
new file mode 100644
index 000000000..18ce2b35f
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_arr2.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun arr () (Array Int Int))
+
+(define-fun A1 () Bool (<= 1 (select arr 0)))
+(define-fun A2 () Bool (<= (select arr 0) (select arr 2)))
+(define-fun A3 () Bool (<= (select arr 2) (+ (select arr 0) 5)))
+(define-fun A4 () Bool (<= 1 (select arr 3)))
+(define-fun A5 () Bool (<= (select arr 3) (select arr 1)))
+(assert (and A1 A2 A3 A4 A5))
+
+;The conjuecture is: 2 <= x+y
+(get-interpol A (<= 2 (+ (select arr 2) (select arr 3))))
diff --git a/test/regress/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/regress1/sygus/interpol_cosa_1.smt2
new file mode 100644
index 000000000..583f94ed4
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_cosa_1.smt2
@@ -0,0 +1,30 @@
+; COMMAND-LINE: --produce-interpols=conjecture --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(set-option :produce-interpols conjecture)
+(set-option :sygus-active-gen enum)
+(declare-fun cfg@1 () (_ BitVec 1))
+(declare-fun witness_0@1 () Bool)
+(declare-fun op@1 () (_ BitVec 4))
+(declare-fun counter@1 () (_ BitVec 16))
+(declare-fun input14@1 () (_ BitVec 1))
+(declare-fun clk@1 () (_ BitVec 1))
+(declare-fun a@1 () (_ BitVec 16))
+(declare-fun b@1 () (_ BitVec 16))
+(reset-assertions)
+(declare-fun cfg@0 () (_ BitVec 1))
+(declare-fun witness_0@0 () Bool)
+(declare-fun counter@0 () (_ BitVec 16))
+(declare-fun op@0 () (_ BitVec 4))
+(declare-fun input14@0 () (_ BitVec 1))
+(declare-fun b@0 () (_ BitVec 16))
+(declare-fun a@0 () (_ BitVec 16))
+(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1)))))
+(assert (and (or (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) witness_0@0) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1)))))
+(declare-fun cfg@2 () (_ BitVec 1))
+(declare-fun counter@2 () (_ BitVec 16))
+(declare-fun op@2 () (_ BitVec 4))
+(declare-fun witness_0@2 () Bool)
+(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1)))))
+(get-interpol I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2))))
diff --git a/test/regress/regress1/sygus/interpol_dt.smt2 b/test/regress/regress1/sygus/interpol_dt.smt2
new file mode 100644
index 000000000..f64ce4a0e
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_dt.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --produce-interpols=default
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
+(declare-fun x () List)
+(declare-fun y () List)
+(assert ((_ is cons) x))
+(assert ((_ is nil) (tail x)))
+(assert (= (head x) 0))
+(assert (= x y))
+(get-interpol A (distinct y nil))
diff --git a/test/regress/regress1/sygus/interpol_from_pono_1.smt2 b/test/regress/regress1/sygus/interpol_from_pono_1.smt2
new file mode 100644
index 000000000..eff00e066
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_from_pono_1.smt2
@@ -0,0 +1,39 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a_S_a2@1 () (_ BitVec 1))
+(declare-fun a_R_a2@1 () (_ BitVec 1))
+(declare-fun a_Q_a2@1 () (_ BitVec 1))
+(declare-fun dve_invalid@1 () (_ BitVec 1))
+(declare-fun v_x1@1 () (_ BitVec 16))
+(declare-fun a_S_a1@1 () (_ BitVec 1))
+(declare-fun v_c@1 () (_ BitVec 16))
+(declare-fun v_x2@1 () (_ BitVec 16))
+(declare-fun a_Q_a1@1 () (_ BitVec 1))
+(declare-fun a_R_a1@1 () (_ BitVec 1))
+(declare-fun f3@1 () (_ BitVec 1))
+(declare-fun f0@1 () (_ BitVec 1))
+(declare-fun f5@1 () (_ BitVec 1))
+(declare-fun f1@1 () (_ BitVec 1))
+(declare-fun f2@1 () (_ BitVec 1))
+(declare-fun f4@1 () (_ BitVec 1))
+(declare-fun dve_invalid@0 () (_ BitVec 1))
+(declare-fun a_S_a2@0 () (_ BitVec 1))
+(declare-fun a_R_a2@0 () (_ BitVec 1))
+(declare-fun a_Q_a2@0 () (_ BitVec 1))
+(declare-fun a_S_a1@0 () (_ BitVec 1))
+(declare-fun a_R_a1@0 () (_ BitVec 1))
+(declare-fun a_Q_a1@0 () (_ BitVec 1))
+(declare-fun v_x2@0 () (_ BitVec 16))
+(declare-fun v_x1@0 () (_ BitVec 16))
+(declare-fun v_c@0 () (_ BitVec 16))
+(declare-fun f5@0 () (_ BitVec 1))
+(declare-fun f3@0 () (_ BitVec 1))
+(declare-fun f4@0 () (_ BitVec 1))
+(declare-fun f2@0 () (_ BitVec 1))
+(declare-fun f0@0 () (_ BitVec 1))
+(declare-fun f1@0 () (_ BitVec 1))
+(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+
+(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1)))))))
diff --git a/test/regress/regress1/sygus/interpol_from_pono_2.smt2 b/test/regress/regress1/sygus/interpol_from_pono_2.smt2
new file mode 100644
index 000000000..894e8e781
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_from_pono_2.smt2
@@ -0,0 +1,41 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a_S_a2@1 () (_ BitVec 1))
+(declare-fun a_R_a2@1 () (_ BitVec 1))
+(declare-fun a_Q_a2@1 () (_ BitVec 1))
+(declare-fun dve_invalid@1 () (_ BitVec 1))
+(declare-fun v_x1@1 () (_ BitVec 16))
+(declare-fun a_S_a1@1 () (_ BitVec 1))
+(declare-fun v_c@1 () (_ BitVec 16))
+(declare-fun v_x2@1 () (_ BitVec 16))
+(declare-fun a_Q_a1@1 () (_ BitVec 1))
+(declare-fun a_R_a1@1 () (_ BitVec 1))
+(declare-fun f3@1 () (_ BitVec 1))
+(declare-fun f0@1 () (_ BitVec 1))
+(declare-fun f5@1 () (_ BitVec 1))
+(declare-fun f1@1 () (_ BitVec 1))
+(declare-fun f2@1 () (_ BitVec 1))
+(declare-fun f4@1 () (_ BitVec 1))
+(declare-fun dve_invalid@0 () (_ BitVec 1))
+(declare-fun a_S_a2@0 () (_ BitVec 1))
+(declare-fun a_R_a2@0 () (_ BitVec 1))
+(declare-fun a_Q_a2@0 () (_ BitVec 1))
+(declare-fun a_S_a1@0 () (_ BitVec 1))
+(declare-fun a_R_a1@0 () (_ BitVec 1))
+(declare-fun a_Q_a1@0 () (_ BitVec 1))
+(declare-fun v_x2@0 () (_ BitVec 16))
+(declare-fun v_x1@0 () (_ BitVec 16))
+(declare-fun v_c@0 () (_ BitVec 16))
+(declare-fun f5@0 () (_ BitVec 1))
+(declare-fun f3@0 () (_ BitVec 1))
+(declare-fun f4@0 () (_ BitVec 1))
+(declare-fun f2@0 () (_ BitVec 1))
+(declare-fun f0@0 () (_ BitVec 1))
+(declare-fun f1@0 () (_ BitVec 1))
+(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+(assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+
+(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1)))))))
+
diff --git a/test/regress/regress1/sygus/interpol_from_pono_3.smt2 b/test/regress/regress1/sygus/interpol_from_pono_3.smt2
new file mode 100644
index 000000000..5de1d4ebd
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_from_pono_3.smt2
@@ -0,0 +1,54 @@
+; COMMAND-LINE: --produce-interpols=default
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a_S_a2@1 () (_ BitVec 1))
+(declare-fun a_R_a2@1 () (_ BitVec 1))
+(declare-fun a_Q_a2@1 () (_ BitVec 1))
+(declare-fun dve_invalid@1 () (_ BitVec 1))
+(declare-fun v_x1@1 () (_ BitVec 16))
+(declare-fun a_S_a1@1 () (_ BitVec 1))
+(declare-fun v_c@1 () (_ BitVec 16))
+(declare-fun v_x2@1 () (_ BitVec 16))
+(declare-fun a_Q_a1@1 () (_ BitVec 1))
+(declare-fun a_R_a1@1 () (_ BitVec 1))
+(declare-fun f3@1 () (_ BitVec 1))
+(declare-fun f0@1 () (_ BitVec 1))
+(declare-fun f5@1 () (_ BitVec 1))
+(declare-fun f1@1 () (_ BitVec 1))
+(declare-fun f2@1 () (_ BitVec 1))
+(declare-fun f4@1 () (_ BitVec 1))
+(declare-fun dve_invalid@0 () (_ BitVec 1))
+(declare-fun a_S_a2@0 () (_ BitVec 1))
+(declare-fun a_R_a2@0 () (_ BitVec 1))
+(declare-fun a_Q_a2@0 () (_ BitVec 1))
+(declare-fun a_S_a1@0 () (_ BitVec 1))
+(declare-fun a_R_a1@0 () (_ BitVec 1))
+(declare-fun a_Q_a1@0 () (_ BitVec 1))
+(declare-fun v_x2@0 () (_ BitVec 16))
+(declare-fun v_x1@0 () (_ BitVec 16))
+(declare-fun v_c@0 () (_ BitVec 16))
+(declare-fun f5@0 () (_ BitVec 1))
+(declare-fun f3@0 () (_ BitVec 1))
+(declare-fun f4@0 () (_ BitVec 1))
+(declare-fun f2@0 () (_ BitVec 1))
+(declare-fun f0@0 () (_ BitVec 1))
+(declare-fun f1@0 () (_ BitVec 1))
+(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+(assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+
+(declare-fun dve_invalid@2 () (_ BitVec 1))
+(declare-fun a_S_a2@2 () (_ BitVec 1))
+(declare-fun a_R_a2@2 () (_ BitVec 1))
+(declare-fun a_Q_a2@2 () (_ BitVec 1))
+(declare-fun a_S_a1@2 () (_ BitVec 1))
+(declare-fun a_R_a1@2 () (_ BitVec 1))
+(declare-fun a_Q_a1@2 () (_ BitVec 1))
+(declare-fun v_x2@2 () (_ BitVec 16))
+(declare-fun v_x1@2 () (_ BitVec 16))
+(declare-fun v_c@2 () (_ BitVec 16))
+(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+
+(get-interpol I (not (and (and true (and (and (and (and (and (and (and (and (and (and true (= v_c@2 (bvxor (_ bv1 16) (ite (= f5@1 (_ bv1 1)) v_x2@1 (ite (= f2@1 (_ bv1 1)) v_x1@1 (bvxor (_ bv1 16) v_c@1)))))) (= v_x1@2 (ite (= f1@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x1@1)))) (= v_x2@2 (ite (= f4@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x2@1)))) (= a_Q_a1@2 (bvnot (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (= a_R_a1@2 (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)))) (= a_S_a1@2 (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)))) (= a_Q_a2@2 (bvnot (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))) (= a_R_a2@2 (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)))) (= a_S_a2@2 (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)))) (= dve_invalid@2 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@1) (bvand (bvnot a_Q_a1@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@1 (bvnot f1@1))) (bvor a_S_a1@1 (bvnot f2@1))) (bvor (bvnot f3@1) (bvand (bvnot a_Q_a2@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@1 (bvnot f4@1))) (bvor a_S_a2@1 (bvnot f5@1))) (bvor f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@1 f1@1) (bvand f2@1 (bvor f0@1 f1@1))) (bvand f3@1 (bvor f2@1 (bvor f0@1 f1@1)))) (bvand f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1))))) (bvand f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@1) a_R_a1@1) (bvand a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1)))) (bvor a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1))) (bvnot (bvor (bvand (bvnot a_Q_a2@1) a_R_a2@1) (bvand a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1))))) (bvor a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)) (bvand (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1))))) (bvor (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)) (bvand (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))))) (bvor (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1))))) (bvnot dve_invalid@1)))))) (not (not (= (bvand (bvnot dve_invalid@2) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@2) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1)))))))
+
+