theory/quantifiers/inst_match_trie.h
theory/quantifiers/inst_strategy_enumerative.cpp
theory/quantifiers/inst_strategy_enumerative.h
+ theory/quantifiers/sygus_inst.cpp
+ theory/quantifiers/sygus_inst.h
theory/quantifiers/instantiate.cpp
theory/quantifiers/instantiate.h
theory/quantifiers/lazy_trie.cpp
type = "bool"
default = "false"
help = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"
+
+
+### SyGuS instantiation options
+
+[[option]]
+ name = "sygusInst"
+ category = "regular"
+ long = "sygus-inst"
+ type = "bool"
+ default = "false"
+ help = "Enable SyGuS instantiation quantifiers module"
if (!smte.isInternalSubsolver())
{
if (options::produceAbducts() || options::sygusInference()
- || options::sygusRewSynthInput())
+ || options::sygusRewSynthInput() || options::sygusInst())
{
// since we are trying to recast as sygus, we assume the input is sygus
is_sygus = true;
d_term_to_anchor[n] = n;
d_anchor_to_conj[n] = d_tds->getConjectureForEnumerator(n);
// this assertion fails if we have a sygus term in the search that is unmeasured
- Assert(d_anchor_to_conj[n] != NULL);
d = 0;
is_top_level = true;
success = true;
if (itc != d_anchor_to_conj.end())
{
quantifiers::SynthConjecture* conj = itc->second;
- Assert(conj != NULL);
- Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds);
- if (!dpred.isNull())
+ if (conj)
{
- sb_lemmas.push_back(dpred);
+ Node dpred =
+ conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds);
+ if (!dpred.isNull())
+ {
+ sb_lemmas.push_back(dpred);
+ }
}
}
}
// get the root (for PBE symmetry breaking)
Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end());
quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a];
- Assert(aconj != NULL);
Trace("sygus-sb-debug") << " ...register search value " << cnv
<< ", type=" << tn << std::endl;
Node bv = d_tds->sygusToBuiltin(cnv, tn);
{
// Is it equivalent under examples?
Node bvr_equiv;
- if (options::sygusSymBreakPbe())
+ if (aconj != nullptr && options::sygusSymBreakPbe())
{
// If the enumerator has examples, see if it is equivalent up to its
// examples with a previous term.
// initialize the term cache
// see if we use an example evaluation cache for symmetry breaking
ExampleEvalCache* eec = nullptr;
- if (options::sygusSymBreakPbe())
+ if (d_parent != nullptr && options::sygusSymBreakPbe())
{
eec = d_parent->getExampleEvalCache(d_enum);
}
// compute the current examples
d_bvr = bvr;
Assert(tds != nullptr);
- ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
- if (eec != nullptr)
+ if (aconj != nullptr)
{
- // get the result of evaluating bvr on the examples of enumerator e.
- eec->evaluateVec(bvr, d_exo, false);
- d_conj = aconj;
- d_enum = e;
+ ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
+ if (eec != nullptr)
+ {
+ // get the result of evaluating bvr on the examples of enumerator e.
+ eec->evaluateVec(bvr, d_exo, false);
+ d_conj = aconj;
+ d_enum = e;
+ }
}
}
};
/** a synthesis conjecture
- * This class implements approaches for a synthesis conecjture, given by data
+ * This class implements approaches for a synthesis conjecture, given by data
* member d_quant.
* This includes both approaches for synthesis in Reynolds et al CAV 2015. It
* determines which approach and optimizations are applicable to the
--- /dev/null
+/********************* */
+/*! \file sygus_inst.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** 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 SyGuS instantiator class.
+ **/
+
+#include "theory/quantifiers/sygus_inst.h"
+
+#include <sstream>
+#include <unordered_set>
+
+#include "expr/node_algorithm.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/sygus_enumerator.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusInst::SygusInst(QuantifiersEngine* qe)
+ : QuantifiersModule(qe),
+ d_lemma_cache(qe->getUserContext()),
+ d_ce_lemma_added(qe->getUserContext())
+{
+}
+
+bool SygusInst::needsCheck(Theory::Effort e)
+{
+ return e >= Theory::EFFORT_LAST_CALL;
+}
+
+QuantifiersModule::QEffort SygusInst::needsModel(Theory::Effort e)
+{
+ return QEFFORT_STANDARD;
+}
+
+void SygusInst::reset_round(Theory::Effort e)
+{
+ d_active_quant.clear();
+ d_inactive_quant.clear();
+
+ FirstOrderModel* model = d_quantEngine->getModel();
+ uint32_t nasserted = model->getNumAssertedQuantifiers();
+
+ for (uint32_t i = 0; i < nasserted; ++i)
+ {
+ Node q = model->getAssertedQuantifier(i);
+
+ if (model->isQuantifierActive(q))
+ {
+ d_active_quant.insert(q);
+ Node lit = getCeLiteral(q);
+
+ bool value;
+ if (d_quantEngine->getValuation().hasSatValue(lit, value))
+ {
+ if (!value)
+ {
+ if (!d_quantEngine->getValuation().isDecision(lit))
+ {
+ model->setQuantifierActive(q, false);
+ d_active_quant.erase(q);
+ d_inactive_quant.insert(q);
+ Trace("sygus-inst") << "Set inactive: " << q << std::endl;
+ }
+ }
+ }
+ }
+ }
+}
+
+void SygusInst::check(Theory::Effort e, QEffort quant_e)
+{
+ Trace("sygus-inst") << "Check " << e << ", " << quant_e << std::endl;
+
+ if (quant_e != QEFFORT_STANDARD) return;
+
+ FirstOrderModel* model = d_quantEngine->getModel();
+ Instantiate* inst = d_quantEngine->getInstantiate();
+ TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
+ SygusExplain syexplain(db);
+ NodeManager* nm = NodeManager::currentNM();
+
+ for (const Node& q : d_active_quant)
+ {
+ std::vector<Node> terms;
+ for (const Node& var : q[0])
+ {
+ Node dt_var = d_inst_constants[var];
+ Node dt_eval = d_var_eval[var];
+ Node value = model->getValue(dt_var);
+ Node t = datatypes::utils::sygusToBuiltin(value);
+ terms.push_back(t);
+
+ std::vector<Node> exp;
+ syexplain.getExplanationForEquality(dt_var, value, exp);
+ Node lem;
+ if (exp.empty())
+ {
+ lem = dt_eval.eqNode(t);
+ }
+ else
+ {
+ lem = nm->mkNode(kind::IMPLIES,
+ exp.size() == 1 ? exp[0] : nm->mkNode(kind::AND, exp),
+ dt_eval.eqNode(t));
+ }
+
+ if (d_lemma_cache.find(lem) == d_lemma_cache.end())
+ {
+ Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
+ d_quantEngine->addLemma(lem, false);
+ d_lemma_cache.insert(lem);
+ }
+ }
+
+ if (inst->addInstantiation(q, terms))
+ {
+ Trace("sygus-inst") << "Instantiate " << q << std::endl;
+ }
+ }
+}
+
+bool SygusInst::checkCompleteFor(Node q)
+{
+ return d_inactive_quant.find(q) != d_inactive_quant.end();
+}
+
+void SygusInst::registerQuantifier(Node q)
+{
+ Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
+
+ Trace("sygus-inst") << "Register " << q << std::endl;
+
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
+ std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+
+ /* Collect extra symbols in 'q' to be used in the grammar. */
+ std::unordered_set<Node, NodeHashFunction> syms;
+ expr::getSymbols(q, syms);
+ for (const TNode& var : syms)
+ {
+ TypeNode tn = var.getType();
+ extra_cons[tn].insert(var);
+ Trace("sygus-inst") << "Found symbol: " << var << std::endl;
+ }
+
+ /* Construct grammar for each bound variable of 'q'. */
+ Trace("sygus-inst") << "Process variables of " << q << std::endl;
+ std::vector<TypeNode> types;
+ for (const Node& var : q[0])
+ {
+ TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(),
+ Node(),
+ var.toString(),
+ extra_cons,
+ exclude_cons,
+ include_cons,
+ term_irrelevant);
+ types.push_back(tn);
+
+ Trace("sygus-inst") << "Construct (default) datatype for " << var
+ << std::endl
+ << tn << std::endl;
+ }
+
+ registerCeLemma(q, types);
+}
+
+/* Construct grammars for all bound variables of quantifier 'q'. Currently,
+ * we use the default grammar of the variable's type.
+ */
+void SygusInst::preRegisterQuantifier(Node q)
+{
+ Trace("sygus-inst") << "preRegister " << q << std::endl;
+ addCeLemma(q);
+}
+
+/*****************************************************************************/
+/* private methods */
+/*****************************************************************************/
+
+Node SygusInst::getCeLiteral(Node q)
+{
+ auto it = d_ce_lits.find(q);
+ if (it != d_ce_lits.end())
+ {
+ return it->second;
+ }
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node sk = nm->mkSkolem("CeLiteral", nm->booleanType());
+ Node lit = d_quantEngine->getValuation().ensureLiteral(sk);
+ d_ce_lits[q] = lit;
+ return lit;
+}
+
+void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
+{
+ Assert(q[0].getNumChildren() == types.size());
+ Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
+
+ /* Generate counterexample lemma for 'q'. */
+ NodeManager* nm = NodeManager::currentNM();
+ TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
+
+ /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
+ * instantiation constant ic_i with type types[i] and wrap each ic_i in
+ * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
+ std::vector<Node> vars;
+ std::vector<Node> evals;
+ for (size_t i = 0, size = types.size(); i < size; ++i)
+ {
+ TypeNode tn = types[i];
+ TNode var = q[0][i];
+
+ /* Create the instantiation constant and set attribute accordingly. */
+ Node ic = nm->mkInstConstant(tn);
+ InstConstantAttribute ica;
+ ic.setAttribute(ica, q);
+
+ db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION);
+
+ std::vector<Node> args = {ic};
+ Node svl = tn.getDType().getSygusVarList();
+ if (!svl.isNull())
+ {
+ args.insert(args.end(), svl.begin(), svl.end());
+ }
+ Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args);
+
+ d_inst_constants.emplace(std::make_pair(var, ic));
+ d_var_eval.emplace(std::make_pair(var, eval));
+
+ vars.push_back(var);
+ evals.push_back(eval);
+ }
+
+ Node lit = getCeLiteral(q);
+ d_quantEngine->addRequirePhase(lit, true);
+
+ /* The decision strategy for quantified formula 'q' ensures that its
+ * counterexample literal is decided on first. It is user-context dependent.
+ */
+ Assert(d_dstrat.find(q) == d_dstrat.end());
+ DecisionStrategy* ds =
+ new DecisionStrategySingleton("CeLiteral",
+ lit,
+ d_quantEngine->getSatContext(),
+ d_quantEngine->getValuation());
+
+ d_dstrat[q].reset(ds);
+ d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy(
+ DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, ds);
+
+ /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
+ Node body =
+ q[1].substitute(vars.begin(), vars.end(), evals.begin(), evals.end());
+ Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate());
+ lem = Rewriter::rewrite(lem);
+
+ d_ce_lemmas.emplace(std::make_pair(q, lem));
+ Trace("sygus-inst") << "Register CE Lemma: " << lem << std::endl;
+}
+
+void SygusInst::addCeLemma(Node q)
+{
+ Assert(d_ce_lemmas.find(q) != d_ce_lemmas.end());
+
+ /* Already added in previous contexts. */
+ if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
+
+ Node lem = d_ce_lemmas[q];
+ d_quantEngine->addLemma(lem, false);
+ d_ce_lemma_added.insert(q);
+ Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file sygus_inst.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** 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 SyGuS instantiator class.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "context/cdhashset.h"
+#include "theory/quantifiers/quant_util.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+
+/**
+ * SyGuS quantifier instantion module.
+ *
+ * This module uses SyGuS techniques to find terms for instantiation and
+ * combines it with counterexample guided instantiation. It uses the datatypes
+ * solver to find instantiation for each variable based on a specified SyGuS
+ * grammar.
+ *
+ * The CE lemma generated for a quantified formula
+ *
+ * \forall x . P[x]
+ *
+ * is
+ *
+ * ce_lit => ~P[DT_SYGUS_EVAL(dt_x)]
+ *
+ * where ce_lit is a the counterexample literal for the quantified formula and
+ * dt_x is a fresh datatype variable with the SyGuS grammar for x as type.
+ *
+ * While checking, for active quantifiers, we add (full) evaluation unfolding
+ * lemmas as follows (see Reynolds at al. CAV 2019b for more information):
+ *
+ * explain(dt_x=dt_x^M) => DT_SYGUS_EVAL(dt_x) = t
+ *
+ * where t = sygusToBuiltin(dt_x^M).
+ *
+ * We collect the t_i for each bound variable x_i and use them to instantiate
+ * the quantified formula.
+ */
+class SygusInst : public QuantifiersModule
+{
+ public:
+ SygusInst(QuantifiersEngine* qe);
+ ~SygusInst() = default;
+
+ bool needsCheck(Theory::Effort e) override;
+
+ QEffort needsModel(Theory::Effort e) override;
+
+ void reset_round(Theory::Effort e) override;
+
+ void check(Theory::Effort e, QEffort quant_e) override;
+
+ bool checkCompleteFor(Node q) override;
+
+ /* Called once for every quantifier 'q' globally (not dependent on context).
+ */
+ void registerQuantifier(Node q) override;
+
+ /* Called once for every quantifier 'q' per context. */
+ void preRegisterQuantifier(Node q) override;
+
+ std::string identify() const override { return "SygusInst"; }
+
+ private:
+ /* Lookup counterexample literal or create a new one for quantifier 'q'. */
+ Node getCeLiteral(Node q);
+
+ /* Generate counterexample lemma for quantifier 'q'. This is done once per
+ * quantifier on registerQuantifier() calls. */
+ void registerCeLemma(Node q, std::vector<TypeNode>& dtypes);
+
+ /* Add counterexample lemma for quantifier 'q'. This is done on every
+ * preRegisterQuantifier() call.*/
+ void addCeLemma(Node q);
+
+ /* Maps bound variables to corresponding instantiation constants. */
+ std::unordered_map<Node, Node, NodeHashFunction> d_inst_constants;
+
+ /* Maps bound variables to corresponding DT_SYGUS_EVAL term. */
+ std::unordered_map<Node, Node, NodeHashFunction> d_var_eval;
+
+ /* Maps quantified formulas to registered counterexample literals. */
+ std::unordered_map<Node, Node, NodeHashFunction> d_ce_lits;
+
+ /* Decision strategies registered for quantified formulas. */
+ std::unordered_map<Node, std::unique_ptr<DecisionStrategy>, NodeHashFunction>
+ d_dstrat;
+
+ /* Currently active quantifiers. */
+ std::unordered_set<Node, NodeHashFunction> d_active_quant;
+
+ /* Currently inactive quantifiers. */
+ std::unordered_set<Node, NodeHashFunction> d_inactive_quant;
+
+ /* Evaluation unfolding lemma. */
+ context::CDHashSet<Node, NodeHashFunction> d_lemma_cache;
+
+ /* Registered counterexample lemma cache. */
+ std::unordered_map<Node, Node, NodeHashFunction> d_ce_lemmas;
+
+ /* Indicates whether a counterexample lemma was added for a quantified
+ * formula in the current context. */
+ context::CDHashSet<Node, NodeHashFunction> d_ce_lemma_added;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif
#include "theory/quantifiers/quant_split.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/sygus_inst.h"
#include "theory/sep/theory_sep.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
d_fs(nullptr),
d_i_cbqi(nullptr),
d_qsplit(nullptr),
- d_anti_skolem(nullptr)
+ d_anti_skolem(nullptr),
+ d_sygus_inst(nullptr)
{
}
~QuantifiersEnginePrivate() {}
std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
/** quantifiers anti-skolemization */
std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
+ /** SyGuS instantiation engine */
+ std::unique_ptr<quantifiers::SygusInst> d_sygus_inst;
//------------------------------ end quantifiers modules
/** initialize
*
d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get()));
modules.push_back(d_fs.get());
}
+ if (options::sygusInst())
+ {
+ d_sygus_inst.reset(new quantifiers::SygusInst(qe));
+ modules.push_back(d_sygus_inst.get());
+ }
}
};
d_util.push_back(d_term_util.get());
d_util.push_back(d_term_db.get());
- if (options::sygus())
+ if (options::sygus() || options::sygusInst())
{
d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
}
regress0/quantifiers/rew-to-scala.smt2
regress0/quantifiers/simp-len.smt2
regress0/quantifiers/simp-typ-test.smt2
+ regress0/quantifiers/sygus-inst-nia-psyco-060.smt2
+ regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
regress0/rec-fun-const-parse-bug.smt2
regress0/rels/addr_book_0.cvc
regress0/rels/atom_univ2.cvc
regress2/quantifiers/net-policy-no-time.smt2
regress2/quantifiers/nunchaku2309663.nun.min.smt2
regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
+ regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
regress2/quantifiers/syn874-1.smt2
regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
regress2/strings/cmu-dis-0707-3.smt2
--- /dev/null
+; COMMAND-LINE: --sygus-inst
+(set-info :smt-lib-version 2.6)
+(set-logic NIA)
+(set-info
+ :source |
+ Generated by PSyCO 0.1
+ More info in N. P. Lopes and J. Monteiro. Weakest Precondition Synthesis for
+ Compiler Optimizations, VMCAI'14.
+|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun W_S1_V6 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun R_S1_V6 () Bool)
+(declare-fun R_S1_V5 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun DISJ_W_S1_R_S1 () Bool)
+(declare-fun W_S1_V5 () Bool)
+(assert
+ (let
+ (($x21121
+ (forall
+ ((V2_0 Int) (V5_0 Int)
+ (V6_0 Int) (MW_S1_V1 Bool)
+ (MW_S1_V3 Bool) (MW_S1_V2 Bool)
+ (MW_S1_V5 Bool) (MW_S1_V6 Bool)
+ (S1_V3_!1741 Int) (S1_V3_!1746 Int)
+ (S1_V1_!1740 Int) (S1_V1_!1745 Int)
+ (S1_V2_!1742 Int) (S1_V2_!1747 Int)
+ (S1_V5_!1743 Int) (S1_V5_!1748 Int)
+ (S1_V6_!1744 Int) (S1_V6_!1749 Int))
+ (let ((?x21214 (ite MW_S1_V6 S1_V6_!1749 V6_0)))
+ (let ((?x21212 (ite MW_S1_V6 S1_V6_!1744 V6_0)))
+ (let (($x21216 (= ?x21212 ?x21214)))
+ (let ((?x21208 (ite MW_S1_V5 S1_V5_!1748 V5_0)))
+ (let ((?x21206 (ite MW_S1_V5 S1_V5_!1743 V5_0)))
+ (let (($x21210 (= ?x21206 ?x21208)))
+ (let ((?x21188 (ite MW_S1_V2 S1_V2_!1747 V2_0)))
+ (let ((?x21174 (ite MW_S1_V2 S1_V2_!1742 V2_0)))
+ (let (($x21204 (= ?x21174 ?x21188)))
+ (let ((?x21198 (+ (- 1) ?x21188)))
+ (let ((?x21052 (ite MW_S1_V3 S1_V3_!1741 0)))
+ (let (($x21202 (= ?x21052 ?x21198)))
+ (let ((?x21060 (ite MW_S1_V1 S1_V1_!1740 0)))
+ (let (($x21200 (= ?x21060 ?x21198)))
+ (let (($x21220 (and $x21200 $x21202 $x21204 $x21210 $x21216)))
+ (let ((?x21190 (* ?x21188 ?x21188)))
+ (let (($x21192 (>= 1 ?x21190)))
+ (let ((?x21182 (* V2_0 V2_0)))
+ (let (($x21184 (<= ?x21182 0)))
+ (let (($x21186 (not $x21184)))
+ (let ((?x21176 (+ (- 1) ?x21174)))
+ (let (($x21180 (>= ?x21060 ?x21176)))
+ (let (($x21178 (>= ?x21052 ?x21176)))
+ (let (($x21170 (<= V2_0 0)))
+ (let (($x21172 (not $x21170)))
+ (let (($x21194 (and $x21172 $x21178 $x21180 $x21186 $x21192)))
+ (let (($x21196 (not $x21194)))
+ (let (($x21078 (not MW_S1_V6)))
+ (let (($x21079 (or $x21078 W_S1_V6)))
+ (let (($x21082 (not MW_S1_V2)))
+ (let (($x21083 (or $x21082 W_S1_V2)))
+ (let (($x21084 (not MW_S1_V3)))
+ (let (($x21085 (or $x21084 W_S1_V3)))
+ (let (($x21086 (not MW_S1_V1)))
+ (let (($x21087 (or $x21086 W_S1_V1)))
+ (let (($x21089 (= S1_V6_!1749 S1_V6_!1744)))
+ (let (($x94 (not R_S1_V3)))
+ (let (($x21141 (or $x94 (= (* (div 0 V2_0) V2_0) 0))))
+ (let ((?x21136 (div 0 V2_0)))
+ (let (($x21137 (= ?x21136 0)))
+ (let (($x92 (not R_S1_V1)))
+ (let (($x21138 (or $x92 $x21137)))
+ (let (($x21144 (not (and $x21138 $x21141))))
+ (let
+ (($x20975
+ (and (or $x21144 (= S1_V3_!1746 S1_V3_!1741))
+ (or $x21144 (= S1_V1_!1745 S1_V1_!1740))
+ (or (not (and (or $x92 (= 0 ?x21136)) $x21141))
+ (= S1_V2_!1742 S1_V2_!1747))
+ (or (not (and (or $x92 (= 0 ?x21136)) $x21141))
+ (= S1_V5_!1743 S1_V5_!1748))
+ (or $x21144 $x21089) $x21087 $x21085 $x21083 $x21079)))
+ (or (not $x20975) $x21196 $x21220))))))))))))))))))))))))))))))))))))))))))))))))
+ (let (($x21 (and W_S1_V6 R_S1_V6)))
+ (let (($x16 (and W_S1_V2 R_S1_V2)))
+ (let (($x13 (and W_S1_V3 R_S1_V3)))
+ (let (($x10 (and W_S1_V1 R_S1_V1)))
+ (let (($x28 (or $x10 $x13 $x16 R_S1_V5 $x21)))
+ (let (($x29 (not $x28)))
+ (let (($x30 (= DISJ_W_S1_R_S1 $x29))) (and W_S1_V5 $x30 $x21121))))))))))
+(assert
+ (let (($x20284 (not W_S1_V2)))
+ (let (($x20278 (not W_S1_V3)))
+ (let (($x20266 (not W_S1_V1)))
+ (let (($x22302 (and $x20266 $x20278 $x20284))) (not $x22302))))))
+(check-sat)
+(exit)
+
--- /dev/null
+; COMMAND-LINE: --sygus-inst --no-check-models
+(set-info :smt-lib-version 2.6)
+(set-logic UFNIA)
+(set-info :source |
+Generated by: Mathias Preiner
+Generated on: 2019-03-22
+Application: Verifying bit-vector rewrite rule candidates independent from bit-width.
+Target solver: CVC4, Z3, Vampire
+Publications: "Towards Bit-Width-Independent Proofs in SMT Solvers " by A. Niemetz, M. Preiner, A. Reynolds, Y. Zohar, C. Barrett, and C. Tinelli, CADE-27 (2019).
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun pow2 (Int) Int)
+(declare-fun intand (Int Int Int) Int)
+(declare-fun intor (Int Int Int) Int)
+(declare-fun intxor (Int Int Int) Int)
+(define-fun bitof ((k Int) (l Int) (a Int)) Int (mod (div a (pow2 l)) 2))
+(define-fun int_all_but_msb ((k Int) (a Int)) Int (mod a (pow2 (- k 1))))
+(define-fun intmax ((k Int)) Int (- (pow2 k) 1))
+(define-fun intmin ((k Int)) Int 0)
+(define-fun in_range ((k Int) (x Int)) Bool (and (>= x 0) (<= x (intmax k))))
+(define-fun intudivtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) (- (pow2 k) 1) (div a b) ))
+(define-fun intmodtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b)))
+(define-fun intneg ((k Int) (a Int)) Int (intmodtotal k (- (pow2 k) a) (pow2 k)))
+(define-fun intnot ((k Int) (a Int)) Int (- (intmax k) a))
+(define-fun intmins ((k Int)) Int (pow2 (- k 1)))
+(define-fun intmaxs ((k Int)) Int (intnot k (intmins k)))
+(define-fun intshl ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a (pow2 b)) (pow2 k)))
+(define-fun intlshr ((k Int) (a Int) (b Int)) Int (intmodtotal k (intudivtotal k a (pow2 b)) (pow2 k)))
+(define-fun intashr ((k Int) (a Int) (b Int) ) Int (ite (= (bitof k (- k 1) a) 0) (intlshr k a b) (intnot k (intlshr k (intnot k a) b))))
+(define-fun intconcat ((k Int) (m Int) (a Int) (b Int)) Int (+ (* a (pow2 m)) b))
+(define-fun intadd ((k Int) (a Int) (b Int) ) Int (intmodtotal k (+ a b) (pow2 k)))
+(define-fun intmul ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a b) (pow2 k)))
+(define-fun intsub ((k Int) (a Int) (b Int)) Int (intadd k a (intneg k b)))
+(define-fun unsigned_to_signed ((k Int) (x Int)) Int (- (* 2 (int_all_but_msb k x)) x))
+(define-fun intslt ((k Int) (a Int) (b Int)) Bool (< (unsigned_to_signed k a) (unsigned_to_signed k b)) )
+(define-fun intsgt ((k Int) (a Int) (b Int)) Bool (> (unsigned_to_signed k a) (unsigned_to_signed k b)) )
+(define-fun intsle ((k Int) (a Int) (b Int)) Bool (<= (unsigned_to_signed k a) (unsigned_to_signed k b)) )
+(define-fun intsge ((k Int) (a Int) (b Int)) Bool (>= (unsigned_to_signed k a) (unsigned_to_signed k b)) )
+(define-fun pow2_base_cases () Bool (and (= (pow2 0) 1) (= (pow2 1) 2) (= (pow2 2) 4) (= (pow2 3) 8) ) )
+;qf axioms
+(define-fun pow2_ax () Bool pow2_base_cases)
+(define-fun and_ax ((k Int)) Bool true)
+(define-fun or_ax ((k Int)) Bool true)
+(define-fun xor_ax ((k Int)) Bool true)
+
+; helpers
+(define-fun is_bv_width ((k Int)) Bool
+ (and
+ (> k 0)
+ (and_ax k)
+ (or_ax k)
+ (xor_ax k)
+ )
+)
+
+(define-fun is_bv_var ((k Int) (x Int)) Bool (in_range k x))
+
+
+; problem start
+(assert pow2_ax)
+(assert (not (forall ((s Int) (t Int) (k Int))
+ (=>
+ (and (is_bv_var k s) (is_bv_var k t) (is_bv_width k))
+ (= (intshl k (intor k t (intnot k t)) t) (intshl k (intnot k (intlshr k s s)) t))
+ )
+ )
+))
+(set-info :status unknown)
+(check-sat)
+(exit)
--- /dev/null
+; COMMAND-LINE: --sygus-inst
+(set-info :smt-lib-version 2.6)
+(set-logic UFBV)
+(set-info :source |
+Hardware fixpoint check problems.
+These benchmarks stem from an evaluation described in Wintersteiger, Hamadi, de Moura: Efficiently solving quantified bit-vector formulas, FMSD 42(1), 2013.
+The hardware models that were used are from the VCEGAR benchmark suite (see www.cprover.org/hardware/).
+|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun Verilog__main.NextState_64_4_39_!127 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.monitor_j_64_1_39_!35 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_fsel_64_4_39_!137 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MDRW_64_2_39_!81 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.JmpE_64_0_39_!21 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.WBSel_64_1_39_!57 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.SESel_64_4_39_!154 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.NPCRW_64_1_39_!44 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.SESel_64_0_39_!26 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ARW_64_1_39_!45 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ZSel_64_1_39_!51 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ARW_64_3_39_!109 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ZSel_64_2_39_!83 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegDst_64_2_39_!86 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_reset_64_3_39_!98 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_j_64_3_39_!99 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_lw_64_0_39_!5 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_bnez_64_3_39_!104 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.State_64_1_39_!30 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.PCRW_64_0_39_!11 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BRW_64_3_39_!110 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.SESel_64_3_39_!122 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRW_64_4_39_!143 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_sw_64_3_39_!100 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegDst_64_4_39_!150 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.State_64_2_39_!62 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.monitor_sw_64_4_39_!132 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRW_64_0_39_!15 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.JmpE_64_3_39_!117 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_lw_64_3_39_!101 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRRW_64_4_39_!138 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BCRW_64_2_39_!82 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_reset_64_1_39_!34 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ARW_64_2_39_!77 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.PCRW_64_3_39_!107 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUOp_64_0_39_!27 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 2))
+(declare-fun Verilog__main.MemRW_64_2_39_!93 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUoutRW_64_0_39_!16 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_lw_64_4_39_!133 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_nop_64_3_39_!102 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegRW_64_0_39_!28 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_j_64_2_39_!67 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_beqz_64_2_39_!71 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.PCRW_64_2_39_!75 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.WBSel_64_4_39_!153 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.NPCRW_64_0_39_!12 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_lw_64_2_39_!69 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_nop_64_2_39_!70 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegDst_64_1_39_!54 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.Reset_64_3_39_!128 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IR_64_0_39_!33 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 32))
+(declare-fun Verilog__main.monitor_reset_64_2_39_!66 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInB_64_2_39_!88 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_beqz_64_4_39_!135 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.SESel_64_1_39_!58 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRRW_64_0_39_!10 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BCRW_64_0_39_!18 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.JmpE_64_4_39_!149 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegDst_64_3_39_!118 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.State_64_0_39_!0 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.NPCRW_64_4_39_!140 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUoutRW_64_4_39_!144 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegRW_64_4_39_!156 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_nop_64_4_39_!134 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_nop_64_1_39_!38 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MemRW_64_1_39_!61 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BCRW_64_1_39_!50 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MDRW_64_4_39_!145 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BCRW_64_4_39_!146 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BRW_64_1_39_!46 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ZSel_64_3_39_!115 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_bnez_64_2_39_!72 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUOp_64_4_39_!155 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 2))
+(declare-fun Verilog__main.monitor_bnez_64_0_39_!8 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BRW_64_2_39_!78 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInB_64_0_39_!24 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.NextState_64_0_39_!1 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.BraE_64_1_39_!52 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_fsel_64_0_39_!9 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IR_64_2_39_!97 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 32))
+(declare-fun Verilog__main.ALUOp_64_3_39_!123 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 2))
+(declare-fun Verilog__main.monitor_beqz_64_1_39_!39 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.JmpE_64_2_39_!85 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_nop_64_0_39_!6 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRRW_64_3_39_!106 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.NPCRW_64_2_39_!76 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.NextState_64_3_39_!95 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.monitor_sw_64_2_39_!68 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_lw_64_1_39_!37 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MemRW_64_4_39_!157 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ARW_64_4_39_!141 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_fsel_64_3_39_!105 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.WBSel_64_3_39_!121 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ZSel_64_0_39_!19 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_fsel_64_1_39_!41 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BraE_64_4_39_!148 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MemRW_64_0_39_!29 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.JmpE_64_1_39_!53 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUoutRW_64_3_39_!112 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_beqz_64_0_39_!7 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegDst_64_0_39_!22 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_sw_64_1_39_!36 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.Reset_64_2_39_!96 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.WBSel_64_0_39_!25 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MDRW_64_0_39_!17 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.NextState_64_2_39_!63 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.IRRW_64_2_39_!74 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInA_64_0_39_!23 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRW_64_3_39_!111 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BraE_64_2_39_!84 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.NextState_64_1_39_!31 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.ALUInA_64_3_39_!119 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IR_64_3_39_!129 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 32))
+(declare-fun Verilog__main.monitor_reset_64_4_39_!130 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.State_64_3_39_!94 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.PCRW_64_4_39_!139 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BCRW_64_3_39_!114 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.WBSel_64_2_39_!89 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BraE_64_0_39_!20 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegRW_64_2_39_!92 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MDRW_64_1_39_!49 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInB_64_1_39_!56 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUoutRW_64_2_39_!80 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.NPCRW_64_3_39_!108 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ZSel_64_4_39_!147 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BRW_64_0_39_!14 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_j_64_0_39_!3 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUOp_64_2_39_!91 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 2))
+(declare-fun Verilog__main.BRW_64_4_39_!142 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRRW_64_1_39_!42 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_beqz_64_3_39_!103 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInA_64_4_39_!151 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_reset_64_0_39_!2 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInB_64_4_39_!152 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUoutRW_64_1_39_!48 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.SESel_64_2_39_!90 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_fsel_64_2_39_!73 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRW_64_1_39_!47 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.BraE_64_3_39_!116 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInB_64_3_39_!120 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.RegRW_64_3_39_!124 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_j_64_4_39_!131 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_bnez_64_1_39_!40 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUOp_64_1_39_!59 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 2))
+(declare-fun Verilog__main.monitor_sw_64_0_39_!4 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MDRW_64_3_39_!113 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.MemRW_64_3_39_!125 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.State_64_4_39_!126 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 6))
+(declare-fun Verilog__main.RegRW_64_1_39_!60 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IRW_64_2_39_!79 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.monitor_bnez_64_4_39_!136 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.IR_64_1_39_!65 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) (_ BitVec 32))
+(declare-fun Verilog__main.PCRW_64_1_39_!43 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInA_64_2_39_!87 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ALUInA_64_1_39_!55 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.ARW_64_0_39_!13 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.Reset_64_1_39_!64 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(declare-fun Verilog__main.Reset_64_0_39_!32 (Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 32) Bool (_ BitVec 6) (_ BitVec 6) Bool Bool (_ BitVec 2) Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool (_ BitVec 6) (_ BitVec 6)) Bool)
+(assert (forall ((Verilog__main.State_64_0 (_ BitVec 6)) (Verilog__main.NextState_64_0 (_ BitVec 6)) (Verilog__main.monitor_reset_64_0 Bool) (Verilog__main.monitor_j_64_0 Bool) (Verilog__main.monitor_sw_64_0 Bool) (Verilog__main.monitor_lw_64_0 Bool) (Verilog__main.monitor_nop_64_0 Bool) (Verilog__main.monitor_beqz_64_0 Bool) (Verilog__main.monitor_bnez_64_0 Bool) (Verilog__main.monitor_fsel_64_0 Bool) (Verilog__main.IRRW_64_0 Bool) (Verilog__main.PCRW_64_0 Bool) (Verilog__main.NPCRW_64_0 Bool) (Verilog__main.ARW_64_0 Bool) (Verilog__main.BRW_64_0 Bool) (Verilog__main.IRW_64_0 Bool) (Verilog__main.ALUoutRW_64_0 Bool) (Verilog__main.MDRW_64_0 Bool) (Verilog__main.BCRW_64_0 Bool) (Verilog__main.ZSel_64_0 Bool) (Verilog__main.BraE_64_0 Bool) (Verilog__main.JmpE_64_0 Bool) (Verilog__main.RegDst_64_0 Bool) (Verilog__main.ALUInA_64_0 Bool) (Verilog__main.ALUInB_64_0 Bool) (Verilog__main.WBSel_64_0 Bool) (Verilog__main.SESel_64_0 Bool) (Verilog__main.ALUOp_64_0 (_ BitVec 2)) (Verilog__main.RegRW_64_0 Bool) (Verilog__main.MemRW_64_0 Bool) (Verilog__main.State_64_1 (_ BitVec 6)) (Verilog__main.NextState_64_1 (_ BitVec 6)) (Verilog__main.Reset_64_0 Bool) (Verilog__main.IR_64_0 (_ BitVec 32)) (Verilog__main.monitor_reset_64_1 Bool) (Verilog__main.monitor_j_64_1 Bool) (Verilog__main.monitor_sw_64_1 Bool) (Verilog__main.monitor_lw_64_1 Bool) (Verilog__main.monitor_nop_64_1 Bool) (Verilog__main.monitor_beqz_64_1 Bool) (Verilog__main.monitor_bnez_64_1 Bool) (Verilog__main.monitor_fsel_64_1 Bool) (Verilog__main.IRRW_64_1 Bool) (Verilog__main.PCRW_64_1 Bool) (Verilog__main.NPCRW_64_1 Bool) (Verilog__main.ARW_64_1 Bool) (Verilog__main.BRW_64_1 Bool) (Verilog__main.IRW_64_1 Bool) (Verilog__main.ALUoutRW_64_1 Bool) (Verilog__main.MDRW_64_1 Bool) (Verilog__main.BCRW_64_1 Bool) (Verilog__main.ZSel_64_1 Bool) (Verilog__main.BraE_64_1 Bool) (Verilog__main.JmpE_64_1 Bool) (Verilog__main.RegDst_64_1 Bool) (Verilog__main.ALUInA_64_1 Bool) (Verilog__main.ALUInB_64_1 Bool) (Verilog__main.WBSel_64_1 Bool) (Verilog__main.SESel_64_1 Bool) (Verilog__main.ALUOp_64_1 (_ BitVec 2)) (Verilog__main.RegRW_64_1 Bool) (Verilog__main.MemRW_64_1 Bool) (Verilog__main.State_64_2 (_ BitVec 6)) (Verilog__main.NextState_64_2 (_ BitVec 6)) (Verilog__main.Reset_64_1 Bool) (Verilog__main.IR_64_1 (_ BitVec 32)) (Verilog__main.monitor_reset_64_2 Bool) (Verilog__main.monitor_j_64_2 Bool) (Verilog__main.monitor_sw_64_2 Bool) (Verilog__main.monitor_lw_64_2 Bool) (Verilog__main.monitor_nop_64_2 Bool) (Verilog__main.monitor_beqz_64_2 Bool) (Verilog__main.monitor_bnez_64_2 Bool) (Verilog__main.monitor_fsel_64_2 Bool) (Verilog__main.IRRW_64_2 Bool) (Verilog__main.PCRW_64_2 Bool) (Verilog__main.NPCRW_64_2 Bool) (Verilog__main.ARW_64_2 Bool) (Verilog__main.BRW_64_2 Bool) (Verilog__main.IRW_64_2 Bool) (Verilog__main.ALUoutRW_64_2 Bool) (Verilog__main.MDRW_64_2 Bool) (Verilog__main.BCRW_64_2 Bool) (Verilog__main.ZSel_64_2 Bool) (Verilog__main.BraE_64_2 Bool) (Verilog__main.JmpE_64_2 Bool) (Verilog__main.RegDst_64_2 Bool) (Verilog__main.ALUInA_64_2 Bool) (Verilog__main.ALUInB_64_2 Bool) (Verilog__main.WBSel_64_2 Bool) (Verilog__main.SESel_64_2 Bool) (Verilog__main.ALUOp_64_2 (_ BitVec 2)) (Verilog__main.RegRW_64_2 Bool) (Verilog__main.MemRW_64_2 Bool) (Verilog__main.State_64_3 (_ BitVec 6)) (Verilog__main.NextState_64_3 (_ BitVec 6)) (Verilog__main.Reset_64_2 Bool) (Verilog__main.IR_64_2 (_ BitVec 32)) (Verilog__main.monitor_reset_64_3 Bool) (Verilog__main.monitor_j_64_3 Bool) (Verilog__main.monitor_sw_64_3 Bool) (Verilog__main.monitor_lw_64_3 Bool) (Verilog__main.monitor_nop_64_3 Bool) (Verilog__main.monitor_beqz_64_3 Bool) (Verilog__main.monitor_bnez_64_3 Bool) (Verilog__main.monitor_fsel_64_3 Bool) (Verilog__main.IRRW_64_3 Bool) (Verilog__main.PCRW_64_3 Bool) (Verilog__main.NPCRW_64_3 Bool) (Verilog__main.ARW_64_3 Bool) (Verilog__main.BRW_64_3 Bool) (Verilog__main.IRW_64_3 Bool) (Verilog__main.ALUoutRW_64_3 Bool) (Verilog__main.MDRW_64_3 Bool) (Verilog__main.BCRW_64_3 Bool) (Verilog__main.ZSel_64_3 Bool) (Verilog__main.BraE_64_3 Bool) (Verilog__main.JmpE_64_3 Bool) (Verilog__main.RegDst_64_3 Bool) (Verilog__main.ALUInA_64_3 Bool) (Verilog__main.ALUInB_64_3 Bool) (Verilog__main.WBSel_64_3 Bool) (Verilog__main.SESel_64_3 Bool) (Verilog__main.ALUOp_64_3 (_ BitVec 2)) (Verilog__main.RegRW_64_3 Bool) (Verilog__main.MemRW_64_3 Bool) (Verilog__main.State_64_4 (_ BitVec 6)) (Verilog__main.NextState_64_4 (_ BitVec 6)) (Verilog__main.Reset_64_3 Bool) (Verilog__main.IR_64_3 (_ BitVec 32)) (Verilog__main.monitor_reset_64_4 Bool) (Verilog__main.monitor_j_64_4 Bool) (Verilog__main.monitor_sw_64_4 Bool) (Verilog__main.monitor_lw_64_4 Bool) (Verilog__main.monitor_nop_64_4 Bool) (Verilog__main.monitor_beqz_64_4 Bool) (Verilog__main.monitor_bnez_64_4 Bool) (Verilog__main.monitor_fsel_64_4 Bool) (Verilog__main.IRRW_64_4 Bool) (Verilog__main.PCRW_64_4 Bool) (Verilog__main.NPCRW_64_4 Bool) (Verilog__main.ARW_64_4 Bool) (Verilog__main.BRW_64_4 Bool) (Verilog__main.IRW_64_4 Bool) (Verilog__main.ALUoutRW_64_4 Bool) (Verilog__main.MDRW_64_4 Bool) (Verilog__main.BCRW_64_4 Bool) (Verilog__main.ZSel_64_4 Bool) (Verilog__main.BraE_64_4 Bool) (Verilog__main.JmpE_64_4 Bool) (Verilog__main.RegDst_64_4 Bool) (Verilog__main.ALUInA_64_4 Bool) (Verilog__main.ALUInB_64_4 Bool) (Verilog__main.WBSel_64_4 Bool) (Verilog__main.SESel_64_4 Bool) (Verilog__main.ALUOp_64_4 (_ BitVec 2)) (Verilog__main.RegRW_64_4 Bool) (Verilog__main.MemRW_64_4 Bool) (Verilog__main.State_64_5 (_ BitVec 6)) (Verilog__main.NextState_64_5 (_ BitVec 6)) (Verilog__main.Reset_64_4 Bool) (Verilog__main.IR_64_4 (_ BitVec 32)) (Verilog__main.monitor_reset_64_5 Bool) (Verilog__main.monitor_j_64_5 Bool) (Verilog__main.monitor_sw_64_5 Bool) (Verilog__main.monitor_lw_64_5 Bool) (Verilog__main.monitor_nop_64_5 Bool) (Verilog__main.monitor_beqz_64_5 Bool) (Verilog__main.monitor_bnez_64_5 Bool) (Verilog__main.monitor_fsel_64_5 Bool) (Verilog__main.IRRW_64_5 Bool) (Verilog__main.PCRW_64_5 Bool) (Verilog__main.NPCRW_64_5 Bool) (Verilog__main.ARW_64_5 Bool) (Verilog__main.BRW_64_5 Bool) (Verilog__main.IRW_64_5 Bool) (Verilog__main.ALUoutRW_64_5 Bool) (Verilog__main.MDRW_64_5 Bool) (Verilog__main.BCRW_64_5 Bool) (Verilog__main.ZSel_64_5 Bool) (Verilog__main.BraE_64_5 Bool) (Verilog__main.JmpE_64_5 Bool) (Verilog__main.RegDst_64_5 Bool) (Verilog__main.ALUInA_64_5 Bool) (Verilog__main.ALUInB_64_5 Bool) (Verilog__main.WBSel_64_5 Bool) (Verilog__main.SESel_64_5 Bool) (Verilog__main.ALUOp_64_5 (_ BitVec 2)) (Verilog__main.RegRW_64_5 Bool) (Verilog__main.MemRW_64_5 Bool)) (=>
projects / cvc5.git / commitdiff