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.
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#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"
d_definedFunctions(nullptr),
d_sygusSolver(nullptr),
d_abductSolver(nullptr),
+ d_interpolSolver(nullptr),
d_quantElimSolver(nullptr),
d_assignments(nullptr),
d_logic(),
{
d_abductSolver.reset(new AbductionSolver(this));
}
+ if (options::produceInterpols() != options::ProduceInterpols::NONE)
+ {
+ d_interpolSolver.reset(new InterpolationSolver(this));
+ }
d_pp->finishInit();
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;
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)
class SmtSolver;
class SygusSolver;
class AbductionSolver;
+class InterpolationSolver;
class QuantElimSolver;
/**
* Representation of a defined function. We keep these around in
/** 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;
/**
}
}
+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
* was successful.
*/
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.
#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 {
SygusInterpol::SygusInterpol() {}
-SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {}
-
void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
const Node& conj)
{
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())
{
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;
}
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;
}
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);
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
const std::vector<Node>& axioms,
const Node& conj,
const TypeNode& itpGType,
- Expr& interpol);
+ Node& interpol);
private:
/**
* @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
*
*/
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.
*/
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
--- /dev/null
+; 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))
+)
+
+)
--- /dev/null
+; 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)))
--- /dev/null
+; 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))
--- /dev/null
+; 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)))
--- /dev/null
+; 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))))
--- /dev/null
+; 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))))
--- /dev/null
+; 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))
--- /dev/null
+; 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)))))))
--- /dev/null
+; 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)))))))
+
--- /dev/null
+; 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)))))))
+
+
projects / cvc5.git / commitdiff