diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9191a7b6..ffac005a 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -109,6 +109,18 @@ if (OPENSMT2_FOUND)
   include_directories(${OPENSMT2_INCLUDE_DIR})
 endif()
 
+# Find Btor2Tools
+SET(BTOR2TOOLS_HOME CACHE STRING "Btor2Tools installation directory")
+find_package(Btor2Tools)
+if (BTOR2TOOLS_FOUND)
+  add_definitions(-DWITH_BTOR2TOOLS)
+  include_directories(${BTOR2TOOLS_INCLUDE_DIRS})
+  set(CMAKE_INSTALL_RPATH "${BTOR2TOOLS_LIBRARY_DIR}")
+  set(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE)
+  set(CMAKE_BUILD_WITH_INSTALL_RPATH TRUE)
+  set(CMAKE_INSTALL_RPATH "${BTOR2TOOLS_HOME}/build/lib")
+endif()
+
 # Make sure antlr C runtime is here
 include(ExternalProject)
 ExternalProject_Add(
diff --git a/README.md b/README.md
index 26e32ede..585f331a 100644
--- a/README.md
+++ b/README.md
@@ -60,6 +60,15 @@ make check
 ```
 You can also set YICES2_HOME, OPENSMT2_HOME, or DREAL_HOME.
 
+To compile with the Btor2 frontend, ensure that you have btor2tools installed 
+(using ``contrib/install_btor2tools.sh``).
+Then provide the BTOR2TOOLS_HOME directory to ``cmake`` and build with  
+```bash
+cd build
+cmake .. -DBTOR2TOOLS_HOME=path/to/contrib/btor2tools
+make
+make check
+```
 
 To compile Sally in debug mode, build with
 ```bash
diff --git a/cmake/FindBtor2Tools.cmake b/cmake/FindBtor2Tools.cmake
new file mode 100644
index 00000000..8f5ecd61
--- /dev/null
+++ b/cmake/FindBtor2Tools.cmake
@@ -0,0 +1,33 @@
+# - Try to find Btor2Tools
+# Once done this will define
+#  BTOR2TOOLS_FOUND - System has Btor2Tools
+#  BTOR2TOOLS_INCLUDE_DIRS - The Btor2Tools include directories
+#  BTOR2TOOLS_LIBRARIES - The libraries needed to use Btor2Tools
+
+if (BTOR2TOOLS_HOME)
+  find_path(BTOR2TOOLS_INCLUDE_DIR btor2parser/btor2parser.h PATHS "${BTOR2TOOLS_HOME}/src" NO_DEFAULT_PATH)
+else()
+  find_path(BTOR2TOOLS_INCLUDE_DIR btor2parser/btor2parser.h)
+endif()
+
+if (SALLY_STATIC_BUILD)
+  if (BTOR2TOOLS_HOME)
+    find_library(BTOR2TOOLS_LIBRARY libbtor2parser.a btor2parser PATHS "${BTOR2TOOLS_HOME}/build/lib" NO_DEFAULT_PATH)
+  else()
+    find_library(BTOR2TOOLS_LIBRARY libbtor2parser.a btor2parser)
+  endif()
+else()
+  if (BTOR2TOOLS_HOME)
+    find_library(BTOR2TOOLS_LIBRARY btor2parser PATHS "${BTOR2TOOLS_HOME}/build/lib" NO_DEFAULT_PATH)
+  else()
+    find_library(BTOR2TOOLS_LIBRARY btor2parser)
+  endif()
+endif()
+
+set(BTOR2TOOLS_LIBRARIES ${BTOR2TOOLS_LIBRARY})
+set(BTOR2TOOLS_INCLUDE_DIRS ${BTOR2TOOLS_INCLUDE_DIR})
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(Btor2Tools DEFAULT_MSG BTOR2TOOLS_LIBRARY BTOR2TOOLS_INCLUDE_DIR)
+
+mark_as_advanced(BTOR2TOOLS_INCLUDE_DIR BTOR2TOOLS_LIBRARY) 
\ No newline at end of file
diff --git a/contrib/install_btor2tools.sh b/contrib/install_btor2tools.sh
new file mode 100755
index 00000000..0c477685
--- /dev/null
+++ b/contrib/install_btor2tools.sh
@@ -0,0 +1,43 @@
+#!/bin/bash
+set -e
+
+echo "Installing btor2tools..."
+
+# Clone the repository
+if ! git clone https://github.com/hwmcc/btor2tools.git; then
+    echo "Error: Failed to clone btor2tools repository." >&2
+    exit 1
+fi
+
+# Navigate to btor2tools directory
+if ! pushd btor2tools; then
+    echo "Error: Failed to enter btor2tools directory." >&2
+    exit 1
+fi
+
+# Run configure script
+if ! ./configure.sh; then
+    echo "Error: Configuration failed." >&2
+    popd > /dev/null 2>&1
+    exit 1
+fi
+
+# Enter build directory
+if ! pushd build; then
+    echo "Error: Failed to enter build directory." >&2
+    popd
+    exit 1
+fi
+
+# Run make
+if ! make; then
+    echo "Error: Build failed." >&2
+    popd; popd
+    exit 1
+fi
+
+# Return to original directories
+popd
+popd
+
+echo "btor2tools installation completed successfully!"
\ No newline at end of file
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 84fa5164..8940e4de 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -47,18 +47,31 @@ endif()
 if (DREAL_FOUND)
   target_link_libraries(sally ${DREAL_LIBRARIES})
 endif()
+if (BTOR2TOOLS_FOUND)
+  target_link_libraries(sally -lbtor2parser)
+endif()
 
 target_link_libraries(sally ${Boost_LIBRARIES} ${GMP_LIBRARY})
 
 # Add tests
 
-file(GLOB_RECURSE regressions 
-  ${sally_SOURCE_DIR}/test/regress/*.mcmt 
-  ${sally_SOURCE_DIR}/test/regress/*.btor
-  ${sally_SOURCE_DIR}/test/regress/*.sal
+# Build the list of regression files based on available solvers
+set(regression_patterns
+  ${sally_SOURCE_DIR}/test/regress/**/*.mcmt 
+  ${sally_SOURCE_DIR}/test/regress/**/*.btor
+  ${sally_SOURCE_DIR}/test/regress/**/*.sal
 )
+
+# Add btor2 files only if Btor2Tools is found
+if (BTOR2TOOLS_FOUND)
+  list(APPEND regression_patterns ${sally_SOURCE_DIR}/test/regress/**/*.btor2)
+endif()
+
+# Get all the regression files
+file(GLOB_RECURSE regressions ${regression_patterns})
 list(SORT regressions)
 
+
 foreach(FILE ${regressions})
   # Get the options for this test
   file(READ "${FILE}.options" ALL_OPTIONS)
diff --git a/src/expr/bitvector.cpp b/src/expr/bitvector.cpp
index b0d3b3d3..0fb3a9f7 100644
--- a/src/expr/bitvector.cpp
+++ b/src/expr/bitvector.cpp
@@ -72,22 +72,28 @@ size_t bitvector::hash() const {
   return hasher.get();
 }
 
-bitvector::bitvector(const char* bits)
-: integer(bits, 2)
-, d_size(strlen(bits))
+bitvector::bitvector(const char* bits, size_t base, size_t size)
+: integer(bits, base)
 {
-  assert(d_size > 0);
+  if (size == 0) {
+    d_size = strlen(bits);
+  } else {
+    d_size = size;
+  }
   assert(sgn() >= 0);
   if (mpz_sizeinbase(d_gmp_int.get_mpz_t(), 2) > d_size) {
     mpz_fdiv_r_2exp(d_gmp_int.get_mpz_t(), d_gmp_int.get_mpz_t(), d_size);
   }
 }
 
-bitvector::bitvector(std::string bits)
-: integer(bits, 2)
-, d_size(bits.size())
+bitvector::bitvector(std::string bits, size_t base, size_t size)
+: integer(bits, base)
 {
-  assert(d_size > 0);
+  if (size == 0) {
+    d_size = bits.size();
+  } else {
+    d_size = size;
+  }
   assert(sgn() >= 0);
   if (mpz_sizeinbase(d_gmp_int.get_mpz_t(), 2) > d_size) {
     mpz_fdiv_r_2exp(d_gmp_int.get_mpz_t(), d_gmp_int.get_mpz_t(), d_size);
diff --git a/src/expr/bitvector.h b/src/expr/bitvector.h
index b295ad84..12f50ef0 100644
--- a/src/expr/bitvector.h
+++ b/src/expr/bitvector.h
@@ -47,11 +47,11 @@ class bitvector : protected integer {
   /** Construct from int */
   bitvector(size_t size, long x);
 
-  /** Construct from a string representation (0 terminated) */
-  explicit bitvector(const char* bits);
+  /** Construct from a string representation ('\0' terminated) */
+  explicit bitvector(const char* bits, size_t base = 2, size_t size = 0);
 
   /** Construct from a string representation */
-  explicit bitvector(std::string bits);
+  explicit bitvector(std::string bits, size_t base = 2, size_t size = 0);
 
   /** Get the size of the bitvector */
   size_t size() const { return d_size; }
diff --git a/src/expr/term.cpp b/src/expr/term.cpp
index 3eee1e0a..0d2434c9 100644
--- a/src/expr/term.cpp
+++ b/src/expr/term.cpp
@@ -140,7 +140,7 @@ void term::mk_let_cache(term_manager& tm, expr_let_cache& let_cache, std::vector
     }
     break;
   default:
-    assert(false);
+    throw exception("Unsupported let caching for operator: " + std::to_string(d_op));
   }
 
   // Record the mapping
@@ -282,7 +282,10 @@ std::string get_smt_keyword(term_op op) {
     return "bvsrem";
   case TERM_BV_SMOD:
     return "bvsmod";
-
+  case TERM_BV_ROR:
+    return "bvror";
+  case TERM_BV_ROL:
+    return "bvrol";
   case TERM_ARRAY_READ:
     return "select";
   case TERM_ARRAY_WRITE:
@@ -660,7 +663,7 @@ void term::to_stream_smt_without_let(std::ostream& out, term_manager& tm, const
     break;
   }
   default:
-    assert(false);
+    throw exception("Unsupported term operation: " + std::to_string(d_op));
   }
 }
 
@@ -695,7 +698,7 @@ std::string get_nuxmv_operator(expr::term_op op) {
   case TERM_BV_UDIV: return "/";
   case TERM_BV_UREM: return "mod";
   default:
-    assert(false);
+    throw exception("Unsupported term operation: " + std::to_string(op));
   }
   return "unknown";
 }
diff --git a/src/expr/term_manager.cpp b/src/expr/term_manager.cpp
index 07ed0c4b..93bf28af 100644
--- a/src/expr/term_manager.cpp
+++ b/src/expr/term_manager.cpp
@@ -874,6 +874,10 @@ term_ref term_manager::mk_or(const std::vector<term_ref>& disjuncts) {
 
 bool term_manager::is_type(term_ref t) const {
   return d_tm->is_type(t);
+} 
+
+bool term_manager::is_boolean_type(term_ref t) const {
+  return d_tm->is_boolean_type(t);
 }
 
 bool term_manager::is_function_type(term_ref t) const {
diff --git a/src/expr/term_manager.h b/src/expr/term_manager.h
index 64dd8daf..f1a9308a 100644
--- a/src/expr/term_manager.h
+++ b/src/expr/term_manager.h
@@ -438,6 +438,9 @@ class term_manager {
   /** Check if t is a type */
   bool is_type(term_ref t) const;
 
+  /** Check if t is a boolean type */
+  bool is_boolean_type(term_ref t) const;
+
   /** Check if t is a function type */
   bool is_function_type(term_ref t) const;
 
diff --git a/src/expr/term_manager_internal.h b/src/expr/term_manager_internal.h
index 571b76d9..c04fa723 100644
--- a/src/expr/term_manager_internal.h
+++ b/src/expr/term_manager_internal.h
@@ -808,9 +808,13 @@ term_ref term_manager_internal::mk_term(term_op op, iterator begin, iterator end
     SWITCH_TO_TERM(TERM_BV_NOR)
     SWITCH_TO_TERM(TERM_BV_XNOR)
     SWITCH_TO_TERM(TERM_BV_CONCAT)
+    SWITCH_TO_TERM(TERM_BV_NEG)
+    SWITCH_TO_TERM(TERM_BV_ROR)
+    SWITCH_TO_TERM(TERM_BV_ROL)
     SWITCH_TO_TERM(TERM_FUN_APP)
     SWITCH_TO_TERM(TERM_TUPLE_CONSTRUCT)
   default:
+    std::cout << "Unsupported term operation: " << op << std::endl;
     assert(false);
   }
 
diff --git a/src/expr/term_ops.cpp b/src/expr/term_ops.cpp
index b295bc83..e08ccca3 100644
--- a/src/expr/term_ops.cpp
+++ b/src/expr/term_ops.cpp
@@ -94,6 +94,10 @@ std::ostream& operator << (std::ostream& out, term_op op) {
     SWITCH_TO_STRING(TERM_BV_UGT)
     SWITCH_TO_STRING(TERM_BV_SGT)
     SWITCH_TO_STRING(TERM_BV_SGN_EXTEND)
+    SWITCH_TO_STRING(TERM_BV_NEG)
+    SWITCH_TO_STRING(TERM_BV_EXTEND)
+    SWITCH_TO_STRING(TERM_BV_ROR)
+    SWITCH_TO_STRING(TERM_BV_ROL)
     SWITCH_TO_STRING(TERM_ARRAY_READ)
     SWITCH_TO_STRING(TERM_ARRAY_WRITE)
     SWITCH_TO_STRING(TERM_ARRAY_LAMBDA)
diff --git a/src/expr/term_ops.h b/src/expr/term_ops.h
index 68c6c3b5..6cb3eb86 100644
--- a/src/expr/term_ops.h
+++ b/src/expr/term_ops.h
@@ -113,6 +113,10 @@ enum term_op {
   TERM_BV_UGT,
   TERM_BV_SGT,
   TERM_BV_SGN_EXTEND,
+  TERM_BV_NEG,
+  TERM_BV_EXTEND,
+  TERM_BV_ROR,
+  TERM_BV_ROL,
 
   // Arrays
   TERM_ARRAY_READ,
diff --git a/src/expr/type_computation_visitor.cpp b/src/expr/type_computation_visitor.cpp
index 58e17fb6..59585c97 100644
--- a/src/expr/type_computation_visitor.cpp
+++ b/src/expr/type_computation_visitor.cpp
@@ -513,6 +513,17 @@ void type_computation_visitor::visit(term_ref t_ref) {
       else error_message << "child must be a bit-vector";
     }
     break;
+  case TERM_BV_NEG:
+    if (t.size() != 1) {
+      d_ok = false;
+      error_message << "must have 1 child";
+    } else {
+      term_ref t0 = base_type_of(t[0]);
+      d_ok = d_tm.is_bitvector_type(t0);
+      if (d_ok) t_type = t0;
+      else error_message << "child must be a bit-vector";
+    }
+    break;
   case TERM_BV_SUB:
     if (t.size() == 1) {
       term_ref t0 = base_type_of(t[0]);
@@ -658,6 +669,7 @@ void type_computation_visitor::visit(term_ref t_ref) {
     }
     break;
   case TERM_BV_SGN_EXTEND:
+  case TERM_BV_EXTEND:
     if (t.size() != 1) {
       d_ok = false;
       error_message << "must have 1 child";
@@ -1007,6 +1019,7 @@ void type_computation_visitor::visit(term_ref t_ref) {
     else error_message << "no children allowed";
     break;
   default:
+    std::cout << "Unsupported term operation: " << t.op() << std::endl;
     assert(false);
   }
 
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 716f0605..399aec78 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -78,7 +78,7 @@ set_source_files_properties(
     COMPILE_FLAGS "-Wno-parentheses-equality -Wno-sign-compare -Wno-unused-function -Wno-unused-variable -Wno-tautological-compare -x c++"
 )
 
-set_source_fileS_properties(
+set_source_files_properties(
   aiger/aiger-1.9.4/aiger.c
   PROPERTIES
     LANGUAGE C
@@ -97,6 +97,7 @@ add_library(parser
   btor/btorLexer.c 
   btor/btor_state.cpp
   btor/btor.cpp
+  btor2/btor2.cpp
   sal/salParser.c 
   sal/salLexer.c 
   sal/sal_state.cpp
diff --git a/src/parser/btor/btor_state.cpp b/src/parser/btor/btor_state.cpp
index eae4a0d0..0250b39a 100644
--- a/src/parser/btor/btor_state.cpp
+++ b/src/parser/btor/btor_state.cpp
@@ -261,13 +261,14 @@ cmd::command* btor_state::finalize() const {
   cmd::command* transition_system_define = new cmd::define_transition_system("T", transition_system);
 
   // Query
+  // We cast the roots to booleans then conjunct them
   std::vector<term_ref> bad_children;
   for (size_t i = 0; i < d_roots.size(); ++ i) {
     term_ref bad = tm().substitute_and_cache(d_roots[i], btor_to_state_var);
+    bad = tm().mk_term(TERM_EQ, bad, d_zero);
     bad_children.push_back(bad);
   }
-  term_ref property = tm().mk_or(bad_children);
-  property = tm().mk_term(TERM_EQ, property, d_zero);
+  term_ref property = tm().mk_and(bad_children);
   system::state_formula* property_formula = new system::state_formula(tm(), state_type, property);
   cmd::command* query = new cmd::query(ctx(), "T", property_formula);
 
diff --git a/src/parser/btor2/btor2.cpp b/src/parser/btor2/btor2.cpp
new file mode 100644
index 00000000..3f48d9c8
--- /dev/null
+++ b/src/parser/btor2/btor2.cpp
@@ -0,0 +1,702 @@
+/**
+ * This file is part of sally.
+ * Copyright (C) 2015 SRI International.
+ *
+ * Sally is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Sally is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with sally.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#include "expr/term_manager.h"
+#include "expr/bitvector.h"
+
+#include "command/declare_state_type.h"
+#include "command/define_transition_system.h"
+#include "command/query.h"
+#include "command/sequence.h"
+
+#include <cassert>
+
+#include "parser/btor2/btor2.h"
+
+#ifdef WITH_BTOR2TOOLS
+
+extern "C"
+{
+#include "btor2parser/btor2parser.h"
+}
+
+namespace sally {
+namespace parser {
+
+std::unordered_map<Btor2Tag, expr::term_op> btor2_tag_to_term_op = {
+  {BTOR2_TAG_add, expr::TERM_BV_ADD},
+  {BTOR2_TAG_and, expr::TERM_BV_AND},
+  {BTOR2_TAG_concat, expr::TERM_BV_CONCAT},
+  {BTOR2_TAG_eq, expr::TERM_EQ},
+  {BTOR2_TAG_iff, expr::TERM_EQ},
+  {BTOR2_TAG_implies, expr::TERM_IMPLIES},
+  {BTOR2_TAG_ite, expr::TERM_ITE},
+  {BTOR2_TAG_mul, expr::TERM_BV_MUL},
+  {BTOR2_TAG_nand, expr::TERM_BV_NAND},
+  {BTOR2_TAG_neg, expr::TERM_BV_NEG},
+  {BTOR2_TAG_nor, expr::TERM_BV_NOR},
+  {BTOR2_TAG_not, expr::TERM_BV_NOT},
+  {BTOR2_TAG_or, expr::TERM_BV_OR},
+  {BTOR2_TAG_read, expr::TERM_ARRAY_READ},
+  {BTOR2_TAG_sdiv, expr::TERM_BV_SDIV},
+  {BTOR2_TAG_sext, expr::TERM_BV_SGN_EXTEND},
+  {BTOR2_TAG_sgt, expr::TERM_BV_SGT},
+  {BTOR2_TAG_sgte, expr::TERM_BV_SGEQ},
+  {BTOR2_TAG_slice, expr::TERM_BV_EXTRACT},
+  {BTOR2_TAG_sll, expr::TERM_BV_SHL},
+  {BTOR2_TAG_slt, expr::TERM_BV_SLT},
+  {BTOR2_TAG_slte, expr::TERM_BV_SLEQ},
+  {BTOR2_TAG_smod, expr::TERM_BV_SMOD},
+  {BTOR2_TAG_sra, expr::TERM_BV_ASHR},
+  {BTOR2_TAG_srem, expr::TERM_BV_SREM},
+  {BTOR2_TAG_srl, expr::TERM_BV_LSHR},
+  {BTOR2_TAG_sub, expr::TERM_BV_SUB},
+  {BTOR2_TAG_udiv, expr::TERM_BV_UDIV},
+  {BTOR2_TAG_ugt, expr::TERM_BV_UGT},
+  {BTOR2_TAG_ugte, expr::TERM_BV_UGEQ},
+  {BTOR2_TAG_ult, expr::TERM_BV_ULT},
+  {BTOR2_TAG_ulte, expr::TERM_BV_ULEQ},
+  {BTOR2_TAG_urem, expr::TERM_BV_UREM},
+  {BTOR2_TAG_write, expr::TERM_ARRAY_WRITE},
+  {BTOR2_TAG_xnor, expr::TERM_BV_XNOR},
+  {BTOR2_TAG_xor, expr::TERM_BV_XOR},
+};
+
+class btor2_parser : public internal_parser_interface {
+
+  /** The term mangager */
+  expr::term_manager& tm;
+
+  /** The context */
+  const system::context& ctx;
+
+  /** File we're parsing */
+  std::string filename;
+
+  /** Line we're parsing */
+  int lineno;
+
+  /** The command we're constructing */
+  cmd::command* command;
+
+  // Map from indices to terms
+  std::vector<expr::term_ref> nodes;
+
+  // List of variables indices.
+  // Input variables are essentially just state variables with no next or init
+  // so we can just use the state variables for both.
+  std::vector<size_t> state_vars;
+
+  typedef std::map<size_t, size_t> var_to_var_map;
+
+  // Map from variables to their init versions
+  var_to_var_map init;
+
+  // Map from variables to their next versions
+  var_to_var_map next;
+
+  // List of root nodes
+  std::vector<expr::term_ref_strong> bad;
+  std::vector<expr::term_ref_strong> constraints;
+
+  /** Bitvector 1 */
+  expr::term_ref_strong one;
+
+  /** Bitvector 0 */
+  expr::term_ref_strong zero;
+
+  /** Set the term */
+  void set_term(size_t index, expr::term_ref term, expr::term_ref type_id);
+
+  /** Add a bitvector type */
+  void add_bv_type(size_t id, size_t size);
+
+  /** Add an array type */
+  void add_array_type(size_t id, size_t index, size_t element);
+
+  /** Get the sort at index */
+  expr::term_ref get_type(size_t index) const;
+
+  /** Get the term at index (negated if negative) */
+  expr::term_ref get_term(int index) const;
+
+  /** Get the term at index (negated if negative), casting to bitvector if necessary */
+  expr::term_ref get_term_bitvector(int index) const;
+
+  /** Get the term at index (negated if negative), casting to boolean if necessary */
+  expr::term_ref get_term_boolean(int index) const;
+
+  /** Get the term at index (negated if negative) with a specific width */
+  size_t get_term_width(int index) const;
+
+  /** Add a state variable */
+  void add_state_var(size_t id, size_t type_id, std::string name);
+
+  /** Set init term of state var */
+  void set_init(size_t id, size_t type_id, size_t var_id, expr::term_ref value);
+
+  /** Set next term of state var */
+  void set_next(size_t id, size_t type_id, size_t var_id, expr::term_ref value);
+
+  /** Add a unary term */
+  void add_unary_term(size_t id, expr::term_op op, size_t type_id, expr::term_ref t);
+
+  /** Add a binary term */
+  void add_binary_term(size_t id, expr::term_op op, size_t type_id, expr::term_ref t1, expr::term_ref t2);
+
+  /** Add a ternary term */
+  void add_ternary_term(size_t id, expr::term_op op, size_t type_id, expr::term_ref t1, expr::term_ref t2, expr::term_ref t3);
+
+  /** Build the transition system from the parsed terms */
+  void build_transition_system();
+
+public:
+  btor2_parser(const system::context& ctx, const char* filename);
+  virtual ~btor2_parser();
+
+  cmd::command* parse_command();
+  int get_current_parser_line() const;
+  int get_current_parser_position() const;
+  std::string get_filename() const;
+};
+
+void btor2_parser::set_term(size_t index, expr::term_ref term, expr::term_ref type_id) {
+  // Ensure size
+  if (index >= nodes.size()) {
+    nodes.resize((index * 2) + 1);
+  }
+  nodes[index] = term;
+}
+
+void btor2_parser::add_bv_type(size_t id, size_t size) {
+  // Ensure size
+  if (id >= nodes.size()) {
+    nodes.resize((id * 2) + 1);
+  }
+  // Remember
+  nodes[id] = tm.bitvector_type(size);
+}
+
+void btor2_parser::add_array_type(size_t id, size_t index, size_t element) {
+  // Ensure size
+  if (id >= nodes.size()) {
+    nodes.resize((id * 2) + 1);
+  }
+  // Remember
+  nodes[id] = tm.array_type(get_type(index), get_type(element));
+}
+
+expr::term_ref btor2_parser::get_type(size_t index) const {
+  return nodes[index];
+}
+
+expr::term_ref btor2_parser::get_term(int index) const {
+  size_t i = index >= 0 ? index : -index;
+  expr::term_ref result = nodes[i];
+  // If the id is negative, negate the term
+  if (index >= 0) {
+    return result;
+  } else {
+    return tm.mk_term(expr::TERM_BV_NOT, result);
+  }
+}
+
+expr::term_ref btor2_parser::get_term_bitvector(int index) const {
+  size_t i = index >= 0 ? index : -index;
+  expr::term_ref result = nodes[i];
+
+  // If the term is a boolean, convert it to a bitvector
+  expr::term_ref type = tm.type_of(result);
+  if (tm.is_boolean_type(type)) {
+    result = tm.mk_term(expr::TERM_ITE, result, one, zero);
+  }
+
+  // If the id is negative, negate the term
+  if (index >= 0) {
+    return result;
+  } else {
+    return tm.mk_term(expr::TERM_BV_NOT, result);
+  }
+}
+
+expr::term_ref btor2_parser::get_term_boolean(int index) const {
+  size_t i = index >= 0 ? index : -index;
+  expr::term_ref result = nodes[i];
+
+  // If the term is a bit-vector, convert it to a boolean
+  expr::term_ref type = tm.type_of(result);
+  if (tm.is_bitvector_type(type)) {
+    result = tm.mk_term(expr::TERM_EQ, result, one);
+  }
+
+  // If the id is negative, negate the term
+  if (index >= 0) {
+    return result;
+  } else {
+    return tm.mk_term(expr::TERM_NOT, result);
+  }
+}
+
+size_t btor2_parser::get_term_width(int index) const {
+  expr::term_ref term = get_term_bitvector(index);
+  if (tm.is_bitvector_type(tm.type_of(term))) {
+    return tm.get_bitvector_size(term);
+  } else {
+    throw parser_exception("Term is not a bitvector", filename, lineno);
+  }
+}
+
+void btor2_parser::add_state_var(size_t id, size_t type_id, std::string name) {
+  expr::term_ref type = get_type(type_id);
+  expr::term_ref term = tm.mk_variable(name, type);
+  set_term(id, term, type);
+  state_vars.push_back(id);
+}
+
+void btor2_parser::set_init(size_t id, size_t type_id, size_t var_id, expr::term_ref value) {
+  var_to_var_map::const_iterator find = init.find(var_id);
+  if (find != init.end()) {
+    throw parser_exception("Init already defined for this variable.", filename, lineno);
+  }
+  expr::term_ref type = get_type(type_id);
+  init[var_id] = id;
+  set_term(id, value, type);
+}
+
+void btor2_parser::set_next(size_t id, size_t type_id, size_t var_id, expr::term_ref value) {
+  expr::term_ref type = get_type(type_id);
+  next[var_id] = id;
+  set_term(id, value, type);
+}
+
+void btor2_parser::add_unary_term(size_t id, expr::term_op op, size_t type_id, expr::term_ref t) {
+  expr::term_ref type = get_type(type_id);
+  expr::term_ref term = tm.mk_term(op, t);
+  set_term(id, term, type);
+}
+
+void btor2_parser::add_binary_term(size_t id, expr::term_op op, size_t type_id, expr::term_ref t1, expr::term_ref t2) {
+  expr::term_ref type = get_type(type_id);
+  expr::term_ref term = tm.mk_term(op, t1, t2);
+  set_term(id, term, type);
+}
+
+void btor2_parser::add_ternary_term(size_t id, expr::term_op op, size_t type_id, expr::term_ref t1, expr::term_ref t2, expr::term_ref t3) {
+  expr::term_ref type = get_type(type_id);
+  expr::term_ref term = tm.mk_term(op, t1, t2, t3);
+  set_term(id, term, type);
+}
+
+void btor2_parser::build_transition_system() {
+  // Construct a dummy input type, need it to construct the state type
+  std::vector<std::string> input_names;
+  std::vector<expr::term_ref> input_types;
+  expr::term_ref input_type_ref = tm.mk_struct_type(input_names, input_types);
+
+  // Create the state type
+  std::vector<std::string> state_names;
+  std::vector<expr::term_ref> state_types;
+
+  for (size_t i = 0; i < state_vars.size(); ++ i) {
+    expr::term_ref var_ref = get_term_bitvector(state_vars[i]);
+    const expr::term& var = tm.term_of(var_ref);
+    state_names.push_back(tm.get_variable_name(var));
+    state_types.push_back(tm.type_of(var));
+  }
+  expr::term_ref state_type_ref = tm.mk_struct_type(state_names, state_types);
+
+  system::state_type* state_type = new system::state_type("state_type", tm, state_type_ref, input_type_ref);
+  cmd::command* state_type_declare = new cmd::declare_state_type("state_type", state_type);
+
+  // Get the state variables
+  const std::vector<expr::term_ref>& sally_current_vars = state_type->get_variables(system::state_type::STATE_CURRENT);
+  const std::vector<expr::term_ref>& sally_next_vars = state_type->get_variables(system::state_type::STATE_NEXT);
+
+  // Create the conversion table from btor vars to input, state, and next vars
+  expr::term_manager::substitution_map btor_to_state_var;
+  for (size_t i = 0; i < state_vars.size(); ++ i) {
+    expr::term_ref btor_var = get_term_bitvector(state_vars[i]);
+    expr::term_ref state_var = sally_current_vars[i];
+    btor_to_state_var[btor_var] = state_var;
+  }
+
+  // Initialize the registers
+  std::vector<expr::term_ref> init_children;
+  for (size_t i = 0; i < state_vars.size(); ++ i) {
+    expr::term_ref state_var = sally_current_vars[i];
+    var_to_var_map::const_iterator find = init.find(state_vars[i]);
+    if (find == init.end()) { continue; } 
+    expr::term_ref init_value = get_term_bitvector(find->second);
+    expr::term_ref eq = tm.mk_term(expr::TERM_EQ, state_var, init_value);
+    init_children.push_back(eq);
+  }
+  expr::term_ref init = tm.mk_and(init_children);
+  init = tm.substitute_and_cache(init, btor_to_state_var);
+  system::state_formula* init_formula = new system::state_formula(tm, state_type, init);
+
+  // Define the transition relation
+  std::vector<expr::term_ref> transition_children;
+  for (size_t i = 0; i < state_vars.size(); ++ i) {
+    expr::term_ref next_var = sally_next_vars[i];
+    var_to_var_map::const_iterator find = next.find(state_vars[i]);
+    if (find == next.end()) { continue; } 
+    expr::term_ref next_value = get_term_bitvector(find->second);
+    expr::term_ref eq = tm.mk_term(expr::TERM_EQ, next_var, next_value);
+    transition_children.push_back(eq);
+  }
+  expr::term_ref transition = tm.mk_and(transition_children);
+  transition = tm.substitute_and_cache(transition, btor_to_state_var);
+  system::transition_formula* transition_formula = new system::transition_formula(tm, state_type, transition);
+
+  // Define the transition system
+  system::transition_system* transition_system = new system::transition_system(state_type, init_formula, transition_formula);
+  cmd::command* transition_system_define = new cmd::define_transition_system("Sys", transition_system);
+
+  // Define any invariants
+  std::vector<expr::term_ref> constraint_children;
+  for (size_t i = 0; i < constraints.size(); ++ i) {
+    expr::term_ref constraint = constraints[i];
+    if (tm.type_of(constraint) != tm.boolean_type()) {
+      constraint = tm.mk_term(expr::TERM_EQ, constraint, one);
+    }
+    constraint_children.push_back(constraint);
+  }
+  expr::term_ref invariant = tm.mk_and(constraint_children);
+  invariant = tm.substitute_and_cache(invariant, btor_to_state_var);
+  system::state_formula* invariant_formula = new system::state_formula(tm, state_type, invariant);
+  transition_system->add_invariant(invariant_formula);
+
+  // Query
+  std::vector<expr::term_ref> bad_children;
+  for (size_t i = 0; i < bad.size(); ++ i) {
+    expr::term_ref bad_term = tm.substitute_and_cache(bad[i], btor_to_state_var);
+    if (tm.type_of(bad_term) != tm.boolean_type()) {
+      bad_term = tm.mk_term(expr::TERM_EQ, bad_term, one);
+    }
+    bad_children.push_back(bad_term);
+  }
+  expr::term_ref property = tm.mk_or(bad_children);
+  property = tm.mk_term(expr::TERM_NOT, property);
+  system::state_formula* property_formula = new system::state_formula(tm, state_type, property);
+  cmd::command* query = new cmd::query(ctx, "Sys", property_formula);
+
+  // Make the final command
+  cmd::sequence* full_command = new cmd::sequence();
+  full_command->push_back(state_type_declare);
+  full_command->push_back(transition_system_define);
+  full_command->push_back(query);
+
+  command = full_command;
+}
+
+btor2_parser::btor2_parser(const system::context& ctx, const char* filename)
+: tm(ctx.tm())
+, ctx(ctx)
+, filename(filename)
+, lineno(0)
+, command(0)
+{
+  one = expr::term_ref_strong(tm, tm.mk_bitvector_constant(expr::bitvector(1, 1)));
+  zero = expr::term_ref_strong(tm, tm.mk_bitvector_constant(expr::bitvector(1, 0)));
+
+  Btor2Parser* parser;
+  Btor2LineIterator it;
+  Btor2Line* line;
+
+  FILE *input_file = fopen(filename, "r");
+  if (!input_file) {
+    throw parser_exception("Error opening file: " + std::string(filename), filename, lineno);
+  }
+
+  parser = btor2parser_new();
+  if (!parser) {
+    throw parser_exception("Error creating btor2 parser", filename, lineno);
+  }
+  if (!btor2parser_read_lines(parser, input_file)) {
+    const char *err = btor2parser_error(parser);
+    throw parser_exception("Error reading btor2 file: " + std::string(err), filename, lineno);
+  }
+
+  std::string symbol;
+  it = btor2parser_iter_init(parser);
+  while ((line = btor2parser_iter_next(&it))) {
+    lineno = line->lineno;
+    switch (line->tag)
+    {
+    case BTOR2_TAG_bad: {
+      expr::term_ref term = get_term_bitvector(line->args[0]);
+      expr::term_ref type = tm.type_of(term);
+      bad.push_back(expr::term_ref_strong(tm, term));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_constraint: {
+      expr::term_ref term = get_term_bitvector(line->args[0]);
+      expr::term_ref type = tm.type_of(term);
+      constraints.push_back(expr::term_ref_strong(tm, term));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_input:
+      if (line->symbol == NULL) {
+        symbol = "input_" + std::to_string(line->id);
+      } else {
+        symbol = line->symbol;
+      }
+      add_state_var(line->id, line->sort.id, symbol);
+      break;
+    case BTOR2_TAG_state:
+      if (line->symbol == NULL) {
+        symbol = "state_" + std::to_string(line->id);
+      } else {
+        symbol = line->symbol;
+      }
+      add_state_var(line->id, line->sort.id, symbol);
+      break;
+    case BTOR2_TAG_init:
+      set_init(line->id, line->sort.id, line->args[0], get_term_bitvector(line->args[1]));
+      break;
+    case BTOR2_TAG_next:
+      set_next(line->id, line->sort.id, line->args[0], get_term_bitvector(line->args[1]));
+      break;
+    case BTOR2_TAG_output:
+      break;
+    case BTOR2_TAG_sort:
+      if (line->sort.tag == BTOR2_TAG_SORT_bitvec) {
+        add_bv_type(line->id, line->sort.bitvec.width);
+      } else {
+        throw parser_exception("Sally does not support const arrays: " + std::string(line->name), filename, lineno);
+      }
+      break;
+    case BTOR2_TAG_one:{
+      expr::term_ref type = get_type(line->sort.id);
+      size_t width = tm.get_bitvector_type_size(type);
+      expr::term_ref term = tm.mk_bitvector_constant(expr::bitvector(width, 1));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_ones: {
+      expr::term_ref type = get_type(line->sort.id);
+      size_t width = tm.get_bitvector_type_size(type);
+      expr::term_ref term = tm.mk_bitvector_constant(expr::bitvector::one(width));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_zero: {
+      expr::term_ref type = get_type(line->sort.id);
+      size_t width = tm.get_bitvector_type_size(type);
+      expr::term_ref term = tm.mk_bitvector_constant(expr::bitvector(width, 0));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_const: {
+      expr::term_ref type = get_type(line->sort.id);
+      expr::term_ref term = tm.mk_bitvector_constant(expr::bitvector(line->constant, 2, line->sort.bitvec.width));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_constd: {
+      expr::term_ref type = get_type(line->sort.id);
+      expr::term_ref term = tm.mk_bitvector_constant(expr::bitvector(line->constant, 10, line->sort.bitvec.width));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_consth: {
+      expr::term_ref type = get_type(line->sort.id);
+      expr::term_ref term = tm.mk_bitvector_constant(expr::bitvector(line->constant, 16, line->sort.bitvec.width));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_neq: {
+      expr::term_ref eq = tm.mk_term(expr::TERM_EQ, get_term_bitvector(line->args[0]), get_term_bitvector(line->args[1]));
+      add_unary_term(line->id, expr::TERM_NOT, line->sort.id, eq);
+      break;
+    }
+    case BTOR2_TAG_iff:
+    case BTOR2_TAG_implies: {
+      add_binary_term(line->id, btor2_tag_to_term_op[line->tag], line->sort.id, 
+                      get_term_boolean(line->args[0]), get_term_boolean(line->args[1]));
+      break;
+    }
+    case BTOR2_TAG_eq:      
+    case BTOR2_TAG_sgt:
+    case BTOR2_TAG_sgte:
+    case BTOR2_TAG_slt:
+    case BTOR2_TAG_slte:
+    case BTOR2_TAG_ugt:
+    case BTOR2_TAG_ugte:
+    case BTOR2_TAG_ult:
+    case BTOR2_TAG_ulte:
+    case BTOR2_TAG_and:
+    case BTOR2_TAG_add:
+    case BTOR2_TAG_concat:
+    case BTOR2_TAG_mul:
+    case BTOR2_TAG_nand:
+    case BTOR2_TAG_nor:
+    case BTOR2_TAG_or:
+    case BTOR2_TAG_read:
+    case BTOR2_TAG_sdiv:
+    case BTOR2_TAG_sll:
+    case BTOR2_TAG_smod:
+    case BTOR2_TAG_sra:
+    case BTOR2_TAG_srem:
+    case BTOR2_TAG_srl:
+    case BTOR2_TAG_sub:
+    case BTOR2_TAG_udiv:
+    case BTOR2_TAG_urem:
+    case BTOR2_TAG_xnor:
+    case BTOR2_TAG_xor:
+      add_binary_term(line->id, btor2_tag_to_term_op[line->tag], line->sort.id, 
+                      get_term_bitvector(line->args[0]), get_term_bitvector(line->args[1]));
+      break;
+    case BTOR2_TAG_sext: {
+      expr::term_ref type = get_type(line->sort.id);
+      expr::term_ref term;
+      size_t amt = line->args[1];
+      if (amt == 0) {
+        term = get_term_bitvector(line->args[0]);
+      } else {
+        expr::bitvector_sgn_extend ext(amt);
+        term = tm.mk_bitvector_sgn_extend(get_term_bitvector(line->args[0]), ext);
+      }
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_uext: {
+      expr::term_ref type = get_type(line->sort.id);
+      expr::term_ref term;
+      size_t amt = line->args[1];
+      if (amt == 0) {
+        term = get_term_bitvector(line->args[0]);
+      } else {
+        expr::term_ref zero_term = tm.mk_bitvector_constant(expr::bitvector(amt, 0));
+        term = tm.mk_term(expr::TERM_BV_CONCAT, zero_term, get_term_bitvector(line->args[0]));
+      }
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_rol: 
+    case BTOR2_TAG_ror:
+    case BTOR2_TAG_saddo:
+    case BTOR2_TAG_smulo:
+    case BTOR2_TAG_ssubo:
+    case BTOR2_TAG_sdivo:
+    case BTOR2_TAG_uaddo:
+    case BTOR2_TAG_umulo:
+    case BTOR2_TAG_usubo:
+      throw parser_exception("Unsupported btor2 tag: " + std::string(line->name), filename, lineno);
+    case BTOR2_TAG_inc: {
+      size_t width = get_term_width(line->args[0]);
+      expr::term_ref one_term = tm.mk_bitvector_constant(expr::bitvector(width, 1));
+      add_binary_term(line->id, expr::TERM_BV_ADD, line->sort.id, 
+                      get_term_bitvector(line->args[0]), one_term);
+      break;
+    }
+    case BTOR2_TAG_dec: {
+      size_t width = get_term_width(line->args[0]);
+      expr::term_ref one_term = tm.mk_bitvector_constant(expr::bitvector(width, 1));
+      add_binary_term(line->id, expr::TERM_BV_SUB, line->sort.id, 
+                      get_term_bitvector(line->args[0]), one_term);
+      break;
+    }
+    case BTOR2_TAG_redand: {
+      size_t arg_width = get_term_width(line->args[0]);
+      expr::term_ref ones_term = tm.mk_bitvector_constant(expr::bitvector(arg_width, (1 << arg_width) - 1));
+      add_binary_term(line->id, expr::TERM_EQ, line->sort.id, get_term_bitvector(line->args[0]), ones_term);
+      break;
+    }
+    case BTOR2_TAG_redor: {
+      size_t arg_width = get_term_width(line->args[0]);
+      expr::term_ref zeros_term = tm.mk_bitvector_constant(expr::bitvector(arg_width, 0));
+      expr::term_ref eq = tm.mk_term(expr::TERM_EQ, get_term_bitvector(line->args[0]), zeros_term);
+      add_unary_term(line->id, expr::TERM_NOT, line->sort.id, eq);
+      break;
+    }
+    case BTOR2_TAG_redxor: {
+      expr::term_ref term = tm.mk_bitvector_extract(get_term_bitvector(line->args[0]), expr::bitvector_extract(line->sort.bitvec.width - 1, line->sort.bitvec.width - 1));
+      for (size_t i = 0; i < line->sort.bitvec.width - 1; ++ i) {
+        expr::term_ref next_term = tm.mk_bitvector_extract(get_term_bitvector(line->args[0]), expr::bitvector_extract(i, i));
+        term = tm.mk_term(expr::TERM_BV_XOR, term, next_term);
+      }
+      set_term(line->id, term, get_type(line->sort.id));
+      break;
+    }
+    case BTOR2_TAG_neg:
+    case BTOR2_TAG_not:
+      add_unary_term(line->id, btor2_tag_to_term_op[line->tag], line->sort.id, get_term_bitvector(line->args[0]));
+      break;
+    case BTOR2_TAG_slice: {
+      expr::term_ref type = get_type(line->sort.id);
+      expr::term_ref term = tm.mk_bitvector_extract(get_term_bitvector(line->args[0]), expr::bitvector_extract(line->args[1], line->args[2]));
+      set_term(line->id, term, type);
+      break;
+    }
+    case BTOR2_TAG_ite: {
+      // cast first arg to bools and then add_ternary_term
+      expr::term_ref t1 = get_term_bitvector(line->args[0]);
+      expr::term_ref t1_bool = tm.mk_term(expr::TERM_EQ, t1, one);
+      add_ternary_term(line->id, btor2_tag_to_term_op[line->tag], line->sort.id, 
+                      t1_bool, get_term_bitvector(line->args[1]), get_term_bitvector(line->args[2]));
+      break;
+    }
+    case BTOR2_TAG_write:
+      add_ternary_term(line->id, btor2_tag_to_term_op[line->tag], line->sort.id, 
+                      get_term_bitvector(line->args[0]), get_term_bitvector(line->args[1]), get_term_bitvector(line->args[2]));
+      break;
+    case BTOR2_TAG_fair:
+      throw parser_exception("Unsupported btor2 tag: fair", filename, lineno);
+    case BTOR2_TAG_justice:
+      throw parser_exception("Unsupported btor2 tag: justice", filename, lineno);
+    default:
+      throw parser_exception("Unsupported btor2 tag: " + std::to_string(line->tag), filename, lineno);
+    }
+  }
+
+  build_transition_system();
+  btor2parser_delete(parser);
+}
+
+btor2_parser::~btor2_parser()
+{  }
+
+cmd::command* btor2_parser::parse_command() {
+  // Just return the saved command, and mark it back to 0
+  cmd::command* result = command;
+  command = 0;
+  return result;
+}
+
+int btor2_parser::get_current_parser_line() const {
+  return 0;
+}
+
+int btor2_parser::get_current_parser_position() const {
+  return 0;
+}
+
+std::string btor2_parser::get_filename() const {
+  return filename;
+}
+
+internal_parser_interface* new_btor2_parser(const system::context& ctx, const char* filename) {
+  return new btor2_parser(ctx, filename);
+}
+
+}
+}
+
+#endif
\ No newline at end of file
diff --git a/src/parser/btor2/btor2.h b/src/parser/btor2/btor2.h
new file mode 100644
index 00000000..d137435d
--- /dev/null
+++ b/src/parser/btor2/btor2.h
@@ -0,0 +1,32 @@
+/**
+ * This file is part of sally.
+ * Copyright (C) 2015 SRI International.
+ *
+ * Sally is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Sally is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with sally.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#pragma once
+
+#include "system/context.h"
+#include "parser/antlr_parser.h"
+
+namespace sally {
+namespace parser {
+
+#ifdef WITH_BTOR2TOOLS
+internal_parser_interface* new_btor2_parser(const system::context& ctx, const char* filename);
+#endif
+
+}
+}
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index e2301208..9a4363ca 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -22,6 +22,9 @@
 #include "mcmt/mcmt.h"
 #include "smt2/smt2.h"
 #include "btor/btor.h"
+#ifdef WITH_BTOR2TOOLS
+#include "btor2/btor2.h"
+#endif
 #include "sal/sal.h"
 #include "aiger/aiger.h"
 
@@ -61,6 +64,13 @@ parser_exception::parser_exception(std::string msg, std::string filename, int li
 , d_pos(pos)
 {}
 
+parser_exception::parser_exception(std::string msg, std::string filename, int line)
+: exception(msg)
+, d_filename(filename)
+, d_line(line)
+, d_pos(-1)
+{}
+
 bool parser_exception::has_line_info() const {
   return d_line != -1;
 }
@@ -79,8 +89,12 @@ std::string parser_exception::get_filename() const {
 
 void parser_exception::to_stream(std::ostream& out) const {
   out << "Parse error: ";
-  if (d_line != -1) {
+  if (d_line != -1 && d_pos != -1) {
     out << get_filename() << ":" << get_line() << ":" << get_position() << ": ";
+  } else if (d_line != -1) {
+    out << get_filename() << ":" << get_line() << ": ";
+  } else {
+    out << get_filename() << ":";
   }
   out << get_message();
 }
@@ -97,6 +111,13 @@ parser::parser(const system::context& ctx, input_language lang, const char* file
   case INPUT_BTOR:
     d_internal = new_btor_parser(ctx, filename);
     break;
+  case INPUT_BTOR2:
+#ifdef WITH_BTOR2TOOLS
+      d_internal = new_btor2_parser(ctx, filename);
+#else
+      throw parser_exception("Btor2Tools is not installed, cannot parse btor2 files");
+#endif
+    break;
   case INPUT_SAL:
     d_internal = new_sal_parser(ctx, filename);
     break;
@@ -134,6 +155,9 @@ input_language parser::guess_language(std::string filename) {
     return INPUT_MCMT;
   } else {
     std::string extension = filename.substr(index + 1);
+    if (extension == "btor2") {
+      return INPUT_BTOR2;
+    }
     if (extension == "btor") {
       return INPUT_BTOR;
     }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index e1b24ae1..3b1fc169 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -51,6 +51,7 @@ class parser_exception : public exception {
 
   /** Create an exception with line information */
   parser_exception(std::string msg, std::string filename, int line, int pos);
+  parser_exception(std::string msg, std::string filename, int line);
 
   /** Returns true if the exception carries line information */
   bool has_line_info() const;
@@ -74,6 +75,7 @@ enum input_language {
   INPUT_MCMT,
   INPUT_SMT2,
   INPUT_BTOR,
+  INPUT_BTOR2,
   INPUT_SAL,
   INPUT_AIGER
 };
diff --git a/src/parser/smt2/smt2_state.h b/src/parser/smt2/smt2_state.h
index 6ebb3160..a96fda42 100644
--- a/src/parser/smt2/smt2_state.h
+++ b/src/parser/smt2/smt2_state.h
@@ -24,9 +24,6 @@
 #include "utils/symbol_table.h"
 #include "command/command.h"
 
-
-#include <iosfwd>
-
 #include <antlr3.h>
 
 namespace sally {
diff --git a/src/system/transition_system.cpp b/src/system/transition_system.cpp
index ad175744..bc914871 100644
--- a/src/system/transition_system.cpp
+++ b/src/system/transition_system.cpp
@@ -29,6 +29,7 @@ transition_system::transition_system(const state_type* state_type, state_formula
 , d_transition_relation(transition_relation)
 {
   d_trace_helper = new trace_helper(state_type);
+  d_invariant = new state_formula(state_type->tm(), state_type, state_type->tm().mk_boolean_constant(true));
 }
 
 void transition_system::to_stream(std::ostream& out) const {
@@ -36,6 +37,7 @@ void transition_system::to_stream(std::ostream& out) const {
   out << "type: " << *d_state_type << std::endl;
   out << "I: " << d_initial_states->get_formula() << std::endl;
   out << "T: " << d_transition_relation->get_formula() << std::endl;
+  out << "Inv: " << d_invariant->get_formula() << std::endl;
   out << "]";
 }
 
@@ -57,6 +59,9 @@ expr::term_ref transition_system::get_transition_relation() const {
     expr::term_ref T = get_transition_assumption();
     transition = d_state_type->tm().mk_term(expr::TERM_AND, transition, T);
   }
+  expr::term_ref Inv = get_invariant();
+  expr::term_ref Inv_next = d_state_type->change_formula_vars(state_type::STATE_CURRENT, state_type::STATE_NEXT, Inv);
+  transition = d_state_type->tm().mk_term(expr::TERM_AND, transition, Inv, Inv_next);
   return transition;
 }
 
@@ -65,6 +70,8 @@ expr::term_ref transition_system::get_initial_states() const {
   if (has_state_assumptions()) {
     I = d_state_type->tm().mk_term(expr::TERM_AND, I, get_state_assumption());
   }
+  expr::term_ref Inv = get_invariant();
+  I = d_state_type->tm().mk_term(expr::TERM_AND, I, Inv);
   return I;
 }
 
@@ -77,7 +84,16 @@ void transition_system::add_assumption(transition_formula* assumption) {
 }
 
 void transition_system::add_invariant(state_formula* invariant) {
-  d_invariants.push_back(invariant);
+  expr::term_ref Inv = d_invariant->get_formula();
+  expr::term_ref Inv_new = invariant->get_formula();
+  expr::term_ref combined = d_state_type->tm().mk_term(expr::TERM_AND, Inv, Inv_new);
+  state_formula* new_invariant = new system::state_formula(d_state_type->tm(), d_state_type, combined);
+  delete d_invariant; 
+  d_invariant = new_invariant;
+}
+
+expr::term_ref transition_system::get_invariant() const {
+  return d_invariant->get_formula();
 }
 
 expr::term_ref transition_system::get_state_assumption() const {
@@ -104,11 +120,9 @@ transition_system::~transition_system() {
   for (size_t i = 0; i < d_assumptions_state.size(); ++ i) {
     delete d_assumptions_state[i];
   }
-  for (size_t i = 0; i < d_invariants.size(); ++ i) {
-    delete d_invariants[i];
-  }
   delete d_initial_states;
   delete d_transition_relation;
+  delete d_invariant;
   delete d_trace_helper;
 }
 
diff --git a/src/system/transition_system.h b/src/system/transition_system.h
index 05c171f0..8c91be2c 100644
--- a/src/system/transition_system.h
+++ b/src/system/transition_system.h
@@ -39,6 +39,9 @@ class transition_system {
   /** The transition formula */
   transition_formula* d_transition_relation;
 
+  /** The invariant formula */
+  state_formula* d_invariant;
+
   /** Any assumptions */
   std::vector<state_formula*> d_assumptions_state;
 
@@ -65,19 +68,14 @@ class transition_system {
     return !d_assumptions_transition.empty();
   }
 
-  /** Invariants */
-  std::vector<state_formula*> d_invariants;
-
-  const std::vector<state_formula*>& get_invariants() const {
-    return d_invariants;
-  }
-
   /** Get the assumptions in one state formula */
   expr::term_ref get_state_assumption() const;
 
   /** Get the assumptions in one transition formula */
   expr::term_ref get_transition_assumption() const;
 
+  /** Get the invariant */
+  expr::term_ref get_invariant() const;
 
   /** The trace helper for this transition system */
   trace_helper* d_trace_helper;
@@ -98,6 +96,9 @@ class transition_system {
   /** Get the whole transition relation (disjunction) */
   expr::term_ref get_transition_relation() const;
 
+  /** Add an invariant (takes over the pointer) */
+  void add_invariant(state_formula* invariant);
+
   /** Get the trace helper */
   trace_helper* get_trace_helper() const;
 
@@ -107,9 +108,6 @@ class transition_system {
   /** Add an assumption on the state type (takes over the pointer) */
   void add_assumption(transition_formula* assumption);
 
-  /** Add an invariant to the system (takes over the pointer) */
-  void add_invariant(state_formula* invariant);
-
   /** Print it to the stream */
   void to_stream(std::ostream& out) const;
 };
diff --git a/test/regress/parser/btor/beem/adding.1.prop1-back-serstep.multi-root.btor b/test/regress/parser/btor/beem/adding.1.prop1-back-serstep.multi-root.btor
new file mode 100644
index 00000000..6d9ffa21
--- /dev/null
+++ b/test/regress/parser/btor/beem/adding.1.prop1-back-serstep.multi-root.btor
@@ -0,0 +1,161 @@
+; Model in BTOR format generated by stepout.py 0.41
+1 var 16 nextv_c
+2 var 16 nextv_x1
+3 var 16 nextv_x2
+4 var 1 nexta_Q_a1
+5 var 1 nexta_R_a1
+6 var 1 nexta_S_a1
+7 var 1 nexta_Q_a2
+8 var 1 nexta_R_a2
+9 var 1 nexta_S_a2
+10 var 1 dve_initialized
+11 var 1 dve_valid
+12 and 1 4 -5
+13 and 1 12 -6
+14 and 1 13 7
+15 and 1 14 -8
+16 and 1 15 -9
+17 constd 16 1
+18 eq 1 17 1
+19 and 1 16 18
+20 constd 16 0
+21 eq 1 20 2
+22 and 1 19 21
+23 eq 1 20 3
+24 and 1 22 23
+25 and 1 11 24
+26 root 1 25
+27 var 16 v_c
+28 next 16 1 27
+29 var 16 v_x1
+30 next 16 2 29
+31 var 16 v_x2
+32 next 16 3 31
+33 var 1 a_Q_a1
+34 next 1 4 33
+35 var 1 a_R_a1
+36 next 1 5 35
+37 var 1 a_S_a1
+38 next 1 6 37
+39 var 1 a_Q_a2
+40 next 1 7 39
+41 var 1 a_R_a2
+42 next 1 8 41
+43 var 1 a_S_a2
+44 next 1 9 43
+45 const 1 1
+46 next 1 10 45
+47 var 1 f0
+48 constd 32 20
+49 constd 16 0
+50 concat 32 27 49
+51 constd 5 16
+52 sra 32 50 51
+53 ulte 1 48 52
+54 and 1 33 -53
+55 or 1 -47 54
+56 or 1 35 47
+57 var 1 f1
+58 or 1 56 -57
+59 and 1 55 58
+60 or 1 37 57
+61 var 1 f2
+62 or 1 60 -61
+63 and 1 59 62
+64 var 1 f3
+65 cond 16 47 27 29
+66 concat 32 65 49
+67 sra 32 66 51
+68 add 32 52 67
+69 slice 16 68 15 0
+70 cond 16 57 69 65
+71 cond 16 61 70 27
+72 concat 32 71 49
+73 sra 32 72 51
+74 ulte 1 48 73
+75 and 1 39 -74
+76 or 1 -64 75
+77 and 1 63 76
+78 or 1 41 64
+79 var 1 f4
+80 or 1 78 -79
+81 and 1 77 80
+82 or 1 43 79
+83 var 1 f5
+84 or 1 82 -83
+85 and 1 81 84
+86 or 1 47 57
+87 or 1 61 86
+88 or 1 64 87
+89 or 1 79 88
+90 or 1 83 89
+91 and 1 85 90
+92 and 1 33 35
+93 or 1 33 35
+94 and 1 37 93
+95 or 1 92 94
+96 or 1 37 93
+97 and 1 -95 96
+98 and 1 39 41
+99 or 1 39 41
+100 and 1 43 99
+101 or 1 98 100
+102 and 1 97 -101
+103 or 1 43 99
+104 and 1 102 103
+105 and 1 91 104
+106 and 1 56 -57
+107 and 1 33 -47
+108 or 1 107 61
+109 and 1 106 108
+110 and 1 60 -61
+111 or 1 106 108
+112 and 1 110 111
+113 or 1 109 112
+114 or 1 110 111
+115 and 1 -113 114
+116 and 1 78 -79
+117 and 1 39 -64
+118 or 1 117 83
+119 and 1 116 118
+120 and 1 82 -83
+121 or 1 116 118
+122 and 1 120 121
+123 or 1 119 122
+124 and 1 115 -123
+125 or 1 120 121
+126 and 1 124 125
+127 and 1 105 126
+128 cond 16 64 71 31
+129 concat 32 128 49
+130 sra 32 129 51
+131 add 32 73 130
+132 slice 16 131 15 0
+133 cond 16 79 132 128
+134 cond 16 83 133 71
+135 eq 1 134 1
+136 and 1 127 135
+137 eq 1 70 2
+138 and 1 136 137
+139 eq 1 133 3
+140 and 1 138 139
+141 eq 1 108 4
+142 and 1 140 141
+143 eq 1 106 5
+144 and 1 142 143
+145 eq 1 110 6
+146 and 1 144 145
+147 eq 1 118 7
+148 and 1 146 147
+149 eq 1 116 8
+150 and 1 148 149
+151 eq 1 120 9
+152 and 1 150 151
+153 and 1 152 11
+154 constd 32 17
+155 eq 1 154 52
+156 cond 1 10 153 155
+157 next 1 11 156
+158 root 1 24
+; End
+
diff --git a/test/regress/parser/btor/beem/adding.1.prop1-back-serstep.multi-root.btor.options b/test/regress/parser/btor/beem/adding.1.prop1-back-serstep.multi-root.btor.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor/beem/adding.1.prop1-back-serstep.multi-root.btor.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/count2.btor2 b/test/regress/parser/btor2/count2.btor2
new file mode 100644
index 00000000..a73874b0
--- /dev/null
+++ b/test/regress/parser/btor2/count2.btor2
@@ -0,0 +1,11 @@
+1 sort bitvec 3
+2 zero 1
+3 state 1 v
+4 init 1 3 2
+5 one 1
+6 add 1 3 5
+7 next 1 3 6
+8 ones 1
+9 sort bitvec 1
+10 eq 9 3 8
+11 bad 10
diff --git a/test/regress/parser/btor2/count2.btor2.options b/test/regress/parser/btor2/count2.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/count2.btor2.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/count4.btor2 b/test/regress/parser/btor2/count4.btor2
new file mode 100644
index 00000000..7c89403b
--- /dev/null
+++ b/test/regress/parser/btor2/count4.btor2
@@ -0,0 +1,11 @@
+1 sort bitvec 4
+2 zero 1
+3 state 1
+4 init 1 3 2
+5 one 1
+6 add 1 3 5
+7 next 1 3 6
+8 ones 1
+9 sort bitvec 1
+10 eq 9 3 8
+11 bad 10
diff --git a/test/regress/parser/btor2/count4.btor2.options b/test/regress/parser/btor2/count4.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/count4.btor2.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/factorial4even.btor2 b/test/regress/parser/btor2/factorial4even.btor2
new file mode 100644
index 00000000..28146327
--- /dev/null
+++ b/test/regress/parser/btor2/factorial4even.btor2
@@ -0,0 +1,26 @@
+; int i = 1, factorial = 1;
+; assert (i <= 2 || !(factorial & 1));
+; for (;;) {
+;   factorial *= i;
+;   i++;
+;   assert (i <= 2 || !(factorial & 1));
+; }
+1 sort bitvec 4
+2 one 1
+3 state 1 factorial
+4 state 1 i
+5 init 1 3 2
+6 init 1 4 2
+7 add 1 4 2
+8 mul 1 3 4
+9 next 1 4 7
+10 next 1 3 8
+11 ones 1
+12 sort bitvec 1
+13 eq 12 4 11
+14 bad 13
+15 slice 12 3 0 0
+16 constd 1 3
+17 ugt 12 4 16
+18 and 12 17 15
+19 bad 18
diff --git a/test/regress/parser/btor2/factorial4even.btor2.options b/test/regress/parser/btor2/factorial4even.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/factorial4even.btor2.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/noninitstate.btor2 b/test/regress/parser/btor2/noninitstate.btor2
new file mode 100644
index 00000000..3f65772a
--- /dev/null
+++ b/test/regress/parser/btor2/noninitstate.btor2
@@ -0,0 +1,18 @@
+1 sort bitvec 1
+2 input 1 turn
+3 state 1 state0
+4 state 1 state1
+5 ite 1 -2 -3 3
+6 ite 1 2 -4 4
+7 next 1 3 5
+8 next 1 4 6
+9 eq 1 3 4
+10 one 1
+11 state 1 initially
+12 init 1 11 10
+13 zero 1
+14 next 1 11 13
+15 implies 1 11 -9
+16 not 1 9
+17 constraint 16
+18 bad 9
diff --git a/test/regress/parser/btor2/noninitstate.btor2.options b/test/regress/parser/btor2/noninitstate.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/noninitstate.btor2.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/ponylink-slaveTXlen-sat.btor2 b/test/regress/parser/btor2/ponylink-slaveTXlen-sat.btor2
new file mode 100644
index 00000000..7b9bb448
--- /dev/null
+++ b/test/regress/parser/btor2/ponylink-slaveTXlen-sat.btor2
@@ -0,0 +1,4180 @@
+; BTOR description generated by Yosys 0.7+439 (git sha1 9337e49, clang 3.8.0-2ubuntu4 -fPIC -Os) for module main.
+1 sort bitvec 1
+2 input 1 clk
+3 input 1 serdes_in
+4 state 1 uut.serdes_en_r
+6 state 1 uut.serdes_out_r
+8 state 1 $formal$ponylink-slaveTXlen-sat.sv:2951$1696_CHECK
+9 const 1 0
+10 state 1 $formal$ponylink-slaveTXlen-sat.sv:2951$1696_EN
+11 init 1 10 9
+12 not 1 8
+13 and 1 10 12
+14 bad 13
+15 state 1 uut.pack_8bits.packer.queue_tvalid
+16 not 1 15
+17 sort bitvec 4
+18 state 17 uut.txrx.reset_counter
+19 redor 1 18
+20 not 1 19
+21 and 1 16 20
+22 uext 1 21 0 in_tready
+23 uext 1 20 0 resetn_out
+24 uext 1 2 0 uut.clk
+25 sort bitvec 9
+26 state 25 uut.pack_8bits.packer.ser_tdata
+27 uext 25 26 0 uut.in_ser_tdata
+28 sort bitvec 8
+29 state 28 uut.txrx.in_fifo_iptr
+30 const 1 1
+31 uext 28 30 7
+32 add 28 29 31
+33 state 28 uut.txrx.peer_out_fifo_iptr
+34 neq 1 32 33
+35 and 1 34 20
+36 uext 1 35 0 uut.in_ser_tready
+37 state 1 uut.pack_8bits.packer.ser_tvalid
+38 uext 1 37 0 uut.in_ser_tvalid
+39 uext 1 21 0 uut.in_tready
+40 state 1 uut.unpack_8bits.unpacker.ser_tready
+41 uext 1 40 0 uut.out_ser_tready
+42 state 28 uut.txrx.out_fifo_iptr
+43 state 28 uut.txrx.out_fifo_optr
+44 neq 1 42 43
+45 and 1 44 20
+46 uext 1 45 0 uut.out_ser_tvalid
+47 uext 1 2 0 uut.pack_8bits.packer.clk
+48 state 1 uut.pack_8bits.packer.queue_send_tuser
+49 state 1 uut.pack_8bits.packer.queue_send_tuser2
+50 state 1 uut.pack_8bits.packer.queue_tlast
+51 state 28 uut.pack_8bits.packer.queue_tuser
+52 uext 1 20 0 uut.pack_8bits.packer.resetn
+53 sort bitvec 32
+54 state 53 uut.pack_8bits.packer.rng
+55 sort bitvec 12
+56 state 55 uut.pack_8bits.packer.rng_counter
+57 sort bitvec 5
+58 state 57 uut.pack_8bits.packer.rng_cursor
+59 uext 1 35 0 uut.pack_8bits.packer.ser_tready
+60 uext 1 21 0 uut.pack_8bits.packer.tready
+61 uext 1 20 0 uut.resetn_out
+62 uext 1 4 0 uut.serdes_en
+63 state 1 uut.txrx.encode_1.encoder.serdes_en
+64 uext 1 63 0 uut.serdes_en_t
+65 uext 1 3 0 uut.serdes_in
+66 state 1 uut.serdes_in_r
+67 uext 1 66 0 uut.serdes_in_t
+68 uext 1 6 0 uut.serdes_out
+69 state 1 uut.txrx.encode_1.encoder.serdes_out
+70 uext 1 69 0 uut.serdes_out_t
+71 state 53 uut.txrx.crc32.lfsr_q
+72 uext 53 71 0 uut.txrx.checksum
+73 state 1 uut.txrx.checksum_lock
+74 not 1 73
+75 state 1 uut.txrx.send_valid
+76 init 1 75 9
+77 state 1 uut.txrx.encode_1.encoder.send_ready
+78 and 1 75 77
+79 ite 1 78 74 9
+80 state 1 uut.txrx.hd_send_mode
+81 not 1 80
+82 state 1 uut.txrx.decode_1.decoder.recv_word_en
+83 and 1 81 82
+84 ite 1 83 30 79
+85 uext 1 84 0 uut.txrx.checksum_enable
+86 state 25 uut.txrx.send_word
+87 sort bitvec 10
+88 state 87 uut.txrx.decode_1.decoder.recv_wbits
+89 slice 1 88 0 0
+90 slice 1 88 1 1
+91 and 1 89 90
+92 slice 1 88 2 2
+93 not 1 92
+94 and 1 91 93
+95 slice 1 88 3 3
+96 not 1 95
+97 and 1 94 96
+98 and 1 92 95
+99 not 1 89
+100 and 1 98 99
+101 not 1 90
+102 and 1 100 101
+103 or 1 97 102
+104 and 1 99 101
+105 or 1 91 104
+106 not 1 105
+107 and 1 93 96
+108 or 1 98 107
+109 not 1 108
+110 and 1 106 109
+111 or 1 103 110
+112 and 1 111 101
+113 and 1 112 93
+114 slice 1 88 4 4
+115 slice 1 88 5 5
+116 eq 1 114 115
+117 and 1 113 116
+118 and 1 106 92
+119 and 1 118 95
+120 and 1 109 89
+121 and 1 120 90
+122 or 1 119 121
+123 and 1 122 115
+124 or 1 117 123
+125 and 1 106 93
+126 and 1 125 96
+127 and 1 109 99
+128 and 1 127 101
+129 or 1 126 128
+130 and 1 129 95
+131 and 1 130 114
+132 and 1 131 115
+133 or 1 124 132
+134 and 1 111 99
+135 and 1 134 93
+136 and 1 135 116
+137 or 1 133 136
+138 not 1 114
+139 and 1 129 138
+140 or 1 137 139
+141 and 1 91 114
+142 and 1 141 115
+143 or 1 140 142
+144 and 1 107 138
+145 not 1 115
+146 and 1 144 145
+147 or 1 143 146
+148 xor 1 89 147
+149 and 1 111 90
+150 and 1 149 92
+151 and 1 150 116
+152 or 1 151 123
+153 or 1 152 132
+154 and 1 111 89
+155 and 1 154 92
+156 and 1 155 116
+157 or 1 153 156
+158 or 1 157 139
+159 or 1 158 142
+160 or 1 159 146
+161 xor 1 90 160
+162 or 1 153 136
+163 or 1 162 139
+164 and 1 104 138
+165 and 1 164 145
+166 or 1 163 165
+167 or 1 166 146
+168 xor 1 92 167
+169 or 1 133 156
+170 or 1 169 139
+171 or 1 170 142
+172 or 1 171 146
+173 xor 1 95 172
+174 and 1 129 145
+175 or 1 117 174
+176 or 1 175 132
+177 or 1 176 136
+178 or 1 177 139
+179 or 1 178 165
+180 or 1 179 146
+181 xor 1 114 180
+182 slice 1 88 9 9
+183 slice 1 88 6 6
+184 not 1 183
+185 and 1 182 184
+186 slice 1 88 8 8
+187 slice 1 88 7 7
+188 not 1 187
+189 or 1 186 188
+190 or 1 92 95
+191 or 1 190 114
+192 or 1 191 115
+193 not 1 192
+194 or 1 189 193
+195 and 1 185 194
+196 not 1 182
+197 and 1 183 196
+198 not 1 186
+199 or 1 198 187
+200 or 1 199 192
+201 and 1 197 200
+202 or 1 195 201
+203 and 1 193 187
+204 and 1 203 186
+205 or 1 202 204
+206 and 1 192 188
+207 and 1 206 198
+208 or 1 205 207
+209 or 1 189 192
+210 and 1 185 209
+211 or 1 199 193
+212 and 1 197 211
+213 or 1 210 212
+214 and 1 192 187
+215 and 1 214 186
+216 or 1 213 215
+217 and 1 193 188
+218 and 1 217 198
+219 or 1 216 218
+220 xor 1 182 186
+221 and 1 184 187
+222 and 1 221 198
+223 and 1 222 182
+224 and 1 223 192
+225 and 1 221 186
+226 and 1 225 196
+227 and 1 226 193
+228 or 1 224 227
+229 and 1 183 188
+230 and 1 229 198
+231 and 1 230 182
+232 and 1 231 192
+233 or 1 228 232
+234 and 1 229 186
+235 and 1 234 196
+236 and 1 235 193
+237 or 1 233 236
+238 not 1 237
+239 and 1 220 238
+240 and 1 225 182
+241 or 1 239 240
+242 and 1 230 196
+243 or 1 241 242
+244 and 1 98 114
+245 and 1 244 115
+246 or 1 245 146
+247 and 1 139 115
+248 and 1 247 187
+249 and 1 248 186
+250 and 1 249 182
+251 or 1 246 250
+252 and 1 122 114
+253 and 1 252 145
+254 and 1 253 188
+255 and 1 254 198
+256 and 1 255 196
+257 or 1 251 256
+258 sort bitvec 2
+259 concat 258 161 148
+260 sort bitvec 3
+261 concat 260 168 259
+262 concat 17 173 261
+263 concat 57 181 262
+264 sort bitvec 6
+265 concat 264 208 263
+266 sort bitvec 7
+267 concat 266 219 265
+268 concat 28 243 267
+269 concat 25 257 268
+270 ite 25 83 269 86
+271 uext 25 270 0 uut.txrx.checksum_word
+272 uext 1 2 0 uut.txrx.clk
+273 uext 1 2 0 uut.txrx.crc32.clk
+274 uext 1 84 0 uut.txrx.crc32.crc_en
+275 uext 53 71 0 uut.txrx.crc32.crc_out
+276 slice 28 270 7 0
+277 not 28 276
+278 slice 1 270 8 8
+279 ite 28 278 277 276
+280 uext 28 279 0 uut.txrx.crc32.data_in
+281 slice 1 71 24 24
+282 slice 1 71 30 30
+283 xor 1 281 282
+284 slice 1 279 0 0
+285 xor 1 283 284
+286 slice 1 279 6 6
+287 xor 1 285 286
+288 slice 1 71 25 25
+289 xor 1 281 288
+290 xor 1 289 282
+291 slice 1 71 31 31
+292 xor 1 290 291
+293 xor 1 292 284
+294 slice 1 279 1 1
+295 xor 1 293 294
+296 xor 1 295 286
+297 slice 1 279 7 7
+298 xor 1 296 297
+299 slice 1 71 26 26
+300 xor 1 289 299
+301 xor 1 300 282
+302 xor 1 301 291
+303 xor 1 302 284
+304 xor 1 303 294
+305 slice 1 279 2 2
+306 xor 1 304 305
+307 xor 1 306 286
+308 xor 1 307 297
+309 xor 1 288 299
+310 slice 1 71 27 27
+311 xor 1 309 310
+312 xor 1 311 291
+313 xor 1 312 294
+314 xor 1 313 305
+315 slice 1 279 3 3
+316 xor 1 314 315
+317 xor 1 316 297
+318 xor 1 281 299
+319 xor 1 318 310
+320 slice 1 71 28 28
+321 xor 1 319 320
+322 xor 1 321 282
+323 xor 1 322 284
+324 xor 1 323 305
+325 xor 1 324 315
+326 slice 1 279 4 4
+327 xor 1 325 326
+328 xor 1 327 286
+329 xor 1 289 310
+330 xor 1 329 320
+331 slice 1 71 29 29
+332 xor 1 330 331
+333 xor 1 332 282
+334 xor 1 333 291
+335 xor 1 334 284
+336 xor 1 335 294
+337 xor 1 336 315
+338 xor 1 337 326
+339 slice 1 279 5 5
+340 xor 1 338 339
+341 xor 1 340 286
+342 xor 1 341 297
+343 xor 1 309 320
+344 xor 1 343 331
+345 xor 1 344 282
+346 xor 1 345 291
+347 xor 1 346 294
+348 xor 1 347 305
+349 xor 1 348 326
+350 xor 1 349 339
+351 xor 1 350 286
+352 xor 1 351 297
+353 xor 1 319 331
+354 xor 1 353 291
+355 xor 1 354 284
+356 xor 1 355 305
+357 xor 1 356 315
+358 xor 1 357 339
+359 xor 1 358 297
+360 slice 1 71 0 0
+361 xor 1 360 281
+362 xor 1 361 288
+363 xor 1 362 310
+364 xor 1 363 320
+365 xor 1 364 284
+366 xor 1 365 294
+367 xor 1 366 315
+368 xor 1 367 326
+369 slice 1 71 1 1
+370 xor 1 369 288
+371 xor 1 370 299
+372 xor 1 371 320
+373 xor 1 372 331
+374 xor 1 373 294
+375 xor 1 374 305
+376 xor 1 375 326
+377 xor 1 376 339
+378 slice 1 71 2 2
+379 xor 1 378 281
+380 xor 1 379 299
+381 xor 1 380 310
+382 xor 1 381 331
+383 xor 1 382 284
+384 xor 1 383 305
+385 xor 1 384 315
+386 xor 1 385 339
+387 slice 1 71 3 3
+388 xor 1 387 281
+389 xor 1 388 288
+390 xor 1 389 310
+391 xor 1 390 320
+392 xor 1 391 284
+393 xor 1 392 294
+394 xor 1 393 315
+395 xor 1 394 326
+396 slice 1 71 4 4
+397 xor 1 396 281
+398 xor 1 397 288
+399 xor 1 398 299
+400 xor 1 399 320
+401 xor 1 400 331
+402 xor 1 401 282
+403 xor 1 402 284
+404 xor 1 403 294
+405 xor 1 404 305
+406 xor 1 405 326
+407 xor 1 406 339
+408 xor 1 407 286
+409 slice 1 71 5 5
+410 xor 1 409 288
+411 xor 1 410 299
+412 xor 1 411 310
+413 xor 1 412 331
+414 xor 1 413 282
+415 xor 1 414 291
+416 xor 1 415 294
+417 xor 1 416 305
+418 xor 1 417 315
+419 xor 1 418 339
+420 xor 1 419 286
+421 xor 1 420 297
+422 slice 1 71 6 6
+423 xor 1 422 299
+424 xor 1 423 310
+425 xor 1 424 320
+426 xor 1 425 282
+427 xor 1 426 291
+428 xor 1 427 305
+429 xor 1 428 315
+430 xor 1 429 326
+431 xor 1 430 286
+432 xor 1 431 297
+433 slice 1 71 7 7
+434 xor 1 433 310
+435 xor 1 434 320
+436 xor 1 435 331
+437 xor 1 436 291
+438 xor 1 437 315
+439 xor 1 438 326
+440 xor 1 439 339
+441 xor 1 440 297
+442 slice 1 71 8 8
+443 xor 1 442 281
+444 xor 1 443 320
+445 xor 1 444 331
+446 xor 1 445 284
+447 xor 1 446 326
+448 xor 1 447 339
+449 slice 1 71 9 9
+450 xor 1 449 288
+451 xor 1 450 331
+452 xor 1 451 282
+453 xor 1 452 294
+454 xor 1 453 339
+455 xor 1 454 286
+456 slice 1 71 10 10
+457 xor 1 456 299
+458 xor 1 457 282
+459 xor 1 458 291
+460 xor 1 459 305
+461 xor 1 460 286
+462 xor 1 461 297
+463 slice 1 71 11 11
+464 xor 1 463 310
+465 xor 1 464 291
+466 xor 1 465 315
+467 xor 1 466 297
+468 slice 1 71 12 12
+469 xor 1 468 320
+470 xor 1 469 326
+471 slice 1 71 13 13
+472 xor 1 471 331
+473 xor 1 472 339
+474 slice 1 71 14 14
+475 xor 1 474 281
+476 xor 1 475 284
+477 slice 1 71 15 15
+478 xor 1 477 281
+479 xor 1 478 288
+480 xor 1 479 282
+481 xor 1 480 284
+482 xor 1 481 294
+483 xor 1 482 286
+484 slice 1 71 16 16
+485 xor 1 484 288
+486 xor 1 485 299
+487 xor 1 486 291
+488 xor 1 487 294
+489 xor 1 488 305
+490 xor 1 489 297
+491 slice 1 71 17 17
+492 xor 1 491 299
+493 xor 1 492 310
+494 xor 1 493 305
+495 xor 1 494 315
+496 slice 1 71 18 18
+497 xor 1 496 281
+498 xor 1 497 310
+499 xor 1 498 320
+500 xor 1 499 282
+501 xor 1 500 284
+502 xor 1 501 315
+503 xor 1 502 326
+504 xor 1 503 286
+505 slice 1 71 19 19
+506 xor 1 505 288
+507 xor 1 506 320
+508 xor 1 507 331
+509 xor 1 508 291
+510 xor 1 509 294
+511 xor 1 510 326
+512 xor 1 511 339
+513 xor 1 512 297
+514 slice 1 71 20 20
+515 xor 1 514 299
+516 xor 1 515 331
+517 xor 1 516 282
+518 xor 1 517 305
+519 xor 1 518 339
+520 xor 1 519 286
+521 slice 1 71 21 21
+522 xor 1 521 310
+523 xor 1 522 282
+524 xor 1 523 291
+525 xor 1 524 315
+526 xor 1 525 286
+527 xor 1 526 297
+528 slice 1 71 22 22
+529 xor 1 528 320
+530 xor 1 529 291
+531 xor 1 530 326
+532 xor 1 531 297
+533 slice 1 71 23 23
+534 xor 1 533 331
+535 xor 1 534 339
+536 concat 258 298 287
+537 concat 260 308 536
+538 concat 17 317 537
+539 concat 57 328 538
+540 concat 264 342 539
+541 concat 266 352 540
+542 concat 28 359 541
+543 concat 25 368 542
+544 concat 87 377 543
+545 sort bitvec 11
+546 concat 545 386 544
+547 concat 55 395 546
+548 sort bitvec 13
+549 concat 548 408 547
+550 sort bitvec 14
+551 concat 550 421 549
+552 sort bitvec 15
+553 concat 552 432 551
+554 sort bitvec 16
+555 concat 554 441 553
+556 sort bitvec 17
+557 concat 556 448 555
+558 sort bitvec 18
+559 concat 558 455 557
+560 sort bitvec 19
+561 concat 560 462 559
+562 sort bitvec 20
+563 concat 562 467 561
+564 sort bitvec 21
+565 concat 564 470 563
+566 sort bitvec 22
+567 concat 566 473 565
+568 sort bitvec 23
+569 concat 568 476 567
+570 sort bitvec 24
+571 concat 570 483 569
+572 sort bitvec 25
+573 concat 572 490 571
+574 sort bitvec 26
+575 concat 574 495 573
+576 sort bitvec 27
+577 concat 576 504 575
+578 sort bitvec 28
+579 concat 578 513 577
+580 sort bitvec 29
+581 concat 580 520 579
+582 sort bitvec 30
+583 concat 582 527 581
+584 sort bitvec 31
+585 concat 584 532 583
+586 concat 53 535 585
+587 uext 53 586 0 uut.txrx.crc32.lfsr_c
+588 const 25 111111100
+589 eq 1 270 588
+590 and 1 589 84
+591 uext 1 590 0 uut.txrx.crc32.rst
+592 uext 1 2 0 uut.txrx.decode_1.decoder.clk
+593 const 17 0000
+594 state 17 uut.txrx.decode_1.decoder.cnt
+595 init 17 594 593
+596 state 17 uut.txrx.decode_1.decoder.cnt2
+597 init 17 596 593
+598 uext 1 2 0 uut.txrx.decode_1.decoder.de8b10b.clk
+599 and 1 91 92
+600 and 1 599 95
+601 and 1 104 93
+602 and 1 601 96
+603 or 1 600 602
+604 and 1 183 187
+605 and 1 604 186
+606 and 1 605 182
+607 or 1 603 606
+608 and 1 184 188
+609 and 1 608 198
+610 and 1 609 196
+611 or 1 607 610
+612 and 1 139 145
+613 or 1 611 612
+614 and 1 252 115
+615 or 1 613 614
+616 and 1 114 115
+617 and 1 616 183
+618 and 1 617 187
+619 and 1 618 186
+620 or 1 615 619
+621 and 1 138 145
+622 and 1 621 184
+623 and 1 622 188
+624 and 1 623 198
+625 or 1 620 624
+626 and 1 114 145
+627 and 1 626 187
+628 and 1 627 186
+629 and 1 628 182
+630 or 1 625 629
+631 and 1 138 115
+632 and 1 631 188
+633 and 1 632 198
+634 and 1 633 196
+635 or 1 630 634
+636 not 1 122
+637 and 1 636 114
+638 and 1 637 145
+639 and 1 638 188
+640 and 1 639 198
+641 and 1 640 196
+642 or 1 635 641
+643 not 1 129
+644 and 1 643 138
+645 and 1 644 115
+646 and 1 645 187
+647 and 1 646 186
+648 and 1 647 182
+649 or 1 642 648
+650 and 1 616 188
+651 and 1 650 198
+652 and 1 651 196
+653 and 1 621 187
+654 and 1 653 186
+655 and 1 654 182
+656 or 1 652 655
+657 or 1 244 144
+658 not 1 657
+659 and 1 656 658
+660 or 1 649 659
+661 or 1 114 115
+662 and 1 122 661
+663 and 1 111 114
+664 and 1 663 115
+665 or 1 662 664
+666 or 1 604 608
+667 not 1 666
+668 and 1 667 186
+669 and 1 668 182
+670 and 1 186 182
+671 and 1 198 196
+672 or 1 670 671
+673 not 1 672
+674 and 1 673 183
+675 and 1 674 187
+676 or 1 669 675
+677 and 1 665 676
+678 or 1 660 677
+679 not 1 616
+680 and 1 129 679
+681 and 1 111 138
+682 and 1 681 145
+683 or 1 680 682
+684 and 1 667 198
+685 and 1 684 196
+686 and 1 673 184
+687 and 1 686 188
+688 or 1 685 687
+689 and 1 683 688
+690 or 1 678 689
+691 and 1 599 138
+692 and 1 691 145
+693 or 1 608 688
+694 and 1 692 693
+695 or 1 690 694
+696 and 1 601 114
+697 and 1 696 115
+698 or 1 604 676
+699 and 1 697 698
+700 or 1 695 699
+701 and 1 604 198
+702 and 1 701 196
+703 and 1 702 665
+704 or 1 700 703
+705 and 1 608 186
+706 and 1 705 182
+707 and 1 706 683
+708 or 1 704 707
+709 and 1 245 184
+710 and 1 709 188
+711 and 1 710 198
+712 or 1 708 711
+713 and 1 146 183
+714 and 1 713 187
+715 and 1 714 186
+716 or 1 712 715
+717 uext 1 716 0 uut.txrx.decode_1.decoder.de8b10b.code_err
+718 uext 87 88 0 uut.txrx.decode_1.decoder.de8b10b.datain
+719 uext 25 269 0 uut.txrx.decode_1.decoder.de8b10b.dataout
+720 uext 1 142 0 uut.txrx.decode_1.decoder.de8b10b.decoder.abei
+721 uext 1 105 0 uut.txrx.decode_1.decoder.de8b10b.decoder.aeqb
+722 uext 1 89 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ai
+723 uext 1 165 0 uut.txrx.decode_1.decoder.de8b10b.decoder.anbnenin
+724 uext 1 148 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ao
+725 uext 1 90 0 uut.txrx.decode_1.decoder.de8b10b.decoder.bi
+726 uext 1 161 0 uut.txrx.decode_1.decoder.de8b10b.decoder.bo
+727 uext 1 108 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ceqd
+728 uext 1 92 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ci
+729 uext 1 146 0 uut.txrx.decode_1.decoder.de8b10b.decoder.cndnenin
+730 uext 1 168 0 uut.txrx.decode_1.decoder.de8b10b.decoder.co
+731 uext 1 716 0 uut.txrx.decode_1.decoder.de8b10b.decoder.code_err
+732 uext 1 147 0 uut.txrx.decode_1.decoder.de8b10b.decoder.compa
+733 uext 1 160 0 uut.txrx.decode_1.decoder.de8b10b.decoder.compb
+734 uext 1 167 0 uut.txrx.decode_1.decoder.de8b10b.decoder.compc
+735 uext 1 172 0 uut.txrx.decode_1.decoder.de8b10b.decoder.compd
+736 uext 1 180 0 uut.txrx.decode_1.decoder.de8b10b.decoder.compe
+737 uext 87 88 0 uut.txrx.decode_1.decoder.de8b10b.decoder.datain
+738 uext 25 269 0 uut.txrx.decode_1.decoder.de8b10b.decoder.dataout
+739 uext 1 95 0 uut.txrx.decode_1.decoder.de8b10b.decoder.di
+740 uext 1 688 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp4n
+741 uext 1 676 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp4p
+742 state 1 uut.txrx.decode_1.decoder.de8b10b.dispout_q
+743 const 266 1111100
+744 uext 87 743 3
+745 neq 1 88 744
+746 and 1 742 745
+747 and 1 111 746
+748 or 1 122 747
+749 uext 1 748 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp6a
+750 not 1 746
+751 and 1 129 750
+752 uext 1 751 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp6a0
+753 and 1 122 746
+754 uext 1 753 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp6a2
+755 not 1 751
+756 and 1 616 755
+757 and 1 748 661
+758 or 1 756 757
+759 or 1 758 753
+760 and 1 616 95
+761 or 1 759 760
+762 or 1 661 95
+763 and 1 761 762
+764 uext 1 763 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp6b
+765 uext 1 683 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp6n
+766 uext 1 665 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp6p
+767 and 1 746 665
+768 and 1 683 750
+769 or 1 767 768
+770 not 1 683
+771 and 1 746 770
+772 and 1 771 183
+773 and 1 772 187
+774 or 1 769 773
+775 and 1 746 89
+776 and 1 775 90
+777 and 1 776 92
+778 or 1 774 777
+779 and 1 771 676
+780 or 1 778 779
+781 not 1 665
+782 and 1 750 781
+783 and 1 782 184
+784 and 1 783 188
+785 or 1 780 784
+786 and 1 750 99
+787 and 1 786 101
+788 and 1 787 93
+789 or 1 785 788
+790 and 1 782 688
+791 or 1 789 790
+792 or 1 791 677
+793 or 1 792 689
+794 uext 1 793 0 uut.txrx.decode_1.decoder.de8b10b.decoder.disp_err
+795 uext 1 746 0 uut.txrx.decode_1.decoder.de8b10b.decoder.dispin
+796 or 1 702 706
+797 and 1 667 673
+798 or 1 796 797
+799 and 1 763 798
+800 or 1 676 799
+801 or 1 800 670
+802 or 1 186 182
+803 and 1 801 802
+804 uext 1 803 0 uut.txrx.decode_1.decoder.de8b10b.decoder.dispout
+805 uext 1 173 0 uut.txrx.decode_1.decoder.de8b10b.decoder.do
+806 uext 1 114 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ei
+807 uext 1 181 0 uut.txrx.decode_1.decoder.de8b10b.decoder.eo
+808 uext 1 666 0 uut.txrx.decode_1.decoder.de8b10b.decoder.feqg
+809 uext 1 798 0 uut.txrx.decode_1.decoder.de8b10b.decoder.fghj22
+810 uext 1 688 0 uut.txrx.decode_1.decoder.de8b10b.decoder.fghjp13
+811 uext 1 676 0 uut.txrx.decode_1.decoder.de8b10b.decoder.fghjp31
+812 uext 1 183 0 uut.txrx.decode_1.decoder.de8b10b.decoder.fi
+813 uext 1 208 0 uut.txrx.decode_1.decoder.de8b10b.decoder.fo
+814 uext 1 187 0 uut.txrx.decode_1.decoder.de8b10b.decoder.gi
+815 uext 1 219 0 uut.txrx.decode_1.decoder.de8b10b.decoder.go
+816 uext 1 672 0 uut.txrx.decode_1.decoder.de8b10b.decoder.heqj
+817 uext 1 186 0 uut.txrx.decode_1.decoder.de8b10b.decoder.hi
+818 uext 1 243 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ho
+819 uext 1 115 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ii
+820 uext 1 182 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ji
+821 uext 1 193 0 uut.txrx.decode_1.decoder.de8b10b.decoder.k28p
+822 uext 1 257 0 uut.txrx.decode_1.decoder.de8b10b.decoder.ko
+823 uext 1 602 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p04
+824 uext 1 129 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p13
+825 uext 1 132 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p13dei
+826 uext 1 139 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p13en
+827 uext 1 174 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p13in
+828 uext 1 111 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p22
+829 uext 1 156 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p22aceeqi
+830 uext 1 136 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p22ancneeqi
+831 uext 1 151 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p22bceeqi
+832 uext 1 117 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p22bncneeqi
+833 uext 1 122 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p31
+834 uext 1 123 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p31i
+835 uext 1 600 0 uut.txrx.decode_1.decoder.de8b10b.decoder.p40
+836 uext 1 793 0 uut.txrx.decode_1.decoder.de8b10b.disp_err
+837 uext 1 746 0 uut.txrx.decode_1.decoder.de8b10b.dispin
+838 uext 1 803 0 uut.txrx.decode_1.decoder.de8b10b.dispout
+839 uext 1 82 0 uut.txrx.decode_1.decoder.de8b10b.enable
+840 or 1 716 793
+841 neq 1 269 588
+842 and 1 840 841
+843 uext 1 842 0 uut.txrx.decode_1.decoder.de8b10b.recv_error
+844 uext 1 63 0 uut.txrx.decode_1.decoder.de8b10b.reset
+845 state 17 uut.txrx.decode_1.decoder.de8b10b.reset_state
+846 state 1 uut.txrx.decode_1.decoder.de8b10b.rstdetect
+847 state 1 uut.txrx.decode_1.decoder.last_bit
+848 init 1 847 9
+849 uext 1 842 0 uut.txrx.decode_1.decoder.recv_error
+850 uext 25 269 0 uut.txrx.decode_1.decoder.recv_word
+851 uext 1 63 0 uut.txrx.decode_1.decoder.reset
+852 uext 1 846 0 uut.txrx.decode_1.decoder.rstdetect
+853 uext 1 66 0 uut.txrx.decode_1.decoder.serdes_in
+854 state 552 uut.txrx.encode_1.encoder.buffer
+855 state 552 uut.txrx.encode_1.encoder.buffer_en
+856 uext 1 2 0 uut.txrx.encode_1.encoder.clk
+857 const 260 000
+858 state 260 uut.txrx.encode_1.encoder.counter
+859 init 260 858 857
+860 uext 1 2 0 uut.txrx.encode_1.encoder.en8b10b.clk
+861 uext 25 86 0 uut.txrx.encode_1.encoder.en8b10b.datain
+862 slice 1 86 0 0
+863 slice 1 86 4 4
+864 slice 1 86 3 3
+865 and 1 863 864
+866 slice 1 86 2 2
+867 not 1 866
+868 and 1 865 867
+869 slice 1 86 1 1
+870 not 1 869
+871 and 1 868 870
+872 not 1 862
+873 and 1 871 872
+874 not 1 863
+875 and 1 862 869
+876 and 1 875 867
+877 not 1 864
+878 and 1 876 877
+879 and 1 866 864
+880 and 1 879 872
+881 and 1 880 870
+882 or 1 878 881
+883 and 1 872 870
+884 or 1 875 883
+885 not 1 884
+886 and 1 867 877
+887 or 1 879 886
+888 not 1 887
+889 and 1 885 888
+890 or 1 882 889
+891 not 1 890
+892 and 1 874 891
+893 and 1 885 866
+894 and 1 893 864
+895 and 1 888 862
+896 and 1 895 869
+897 or 1 894 896
+898 not 1 897
+899 and 1 892 898
+900 or 1 873 899
+901 state 1 uut.txrx.encode_1.encoder.send_disp
+902 neq 1 86 588
+903 and 1 901 902
+904 not 1 903
+905 and 1 900 904
+906 slice 1 86 8 8
+907 and 1 863 891
+908 and 1 885 867
+909 and 1 908 877
+910 and 1 888 872
+911 and 1 910 870
+912 or 1 909 911
+913 not 1 912
+914 and 1 907 913
+915 or 1 906 914
+916 and 1 874 877
+917 and 1 916 866
+918 and 1 917 869
+919 and 1 918 862
+920 or 1 915 919
+921 and 1 920 903
+922 or 1 905 921
+923 xor 1 862 922
+924 and 1 875 866
+925 and 1 924 864
+926 not 1 925
+927 and 1 869 926
+928 and 1 883 867
+929 and 1 928 877
+930 or 1 927 929
+931 xor 1 930 922
+932 or 1 929 866
+933 or 1 932 873
+934 xor 1 933 922
+935 not 1 924
+936 and 1 864 935
+937 xor 1 936 922
+938 or 1 863 912
+939 not 1 873
+940 and 1 938 939
+941 xor 1 940 922
+942 and 1 890 874
+943 and 1 863 877
+944 and 1 943 867
+945 not 1 875
+946 and 1 944 945
+947 or 1 942 946
+948 and 1 863 925
+949 or 1 947 948
+950 and 1 906 863
+951 and 1 950 864
+952 and 1 951 866
+953 and 1 952 870
+954 and 1 953 872
+955 or 1 949 954
+956 and 1 943 866
+957 and 1 956 870
+958 and 1 957 872
+959 or 1 955 958
+960 xor 1 959 922
+961 slice 1 86 5 5
+962 slice 1 86 6 6
+963 and 1 961 962
+964 slice 1 86 7 7
+965 and 1 963 964
+966 and 1 943 912
+967 and 1 874 864
+968 and 1 967 897
+969 ite 1 903 968 966
+970 or 1 906 969
+971 and 1 965 970
+972 not 1 971
+973 and 1 961 972
+974 not 1 961
+975 not 1 962
+976 and 1 974 975
+977 and 1 961 975
+978 and 1 974 962
+979 or 1 977 978
+980 and 1 906 979
+981 or 1 976 980
+982 or 1 900 915
+983 xor 1 903 982
+984 not 1 983
+985 and 1 981 984
+986 and 1 963 983
+987 or 1 985 986
+988 xor 1 973 987
+989 not 1 964
+990 and 1 976 989
+991 or 1 962 990
+992 xor 1 991 987
+993 xor 1 964 987
+994 xor 1 962 961
+995 and 1 989 994
+996 or 1 995 971
+997 xor 1 996 987
+998 concat 258 931 923
+999 concat 260 934 998
+1000 concat 17 937 999
+1001 concat 57 941 1000
+1002 concat 264 960 1001
+1003 concat 266 988 1002
+1004 concat 28 992 1003
+1005 concat 25 993 1004
+1006 concat 87 997 1005
+1007 state 1 uut.txrx.encode_1.encoder.en8b10b.lastbit
+1008 not 1 1007
+1009 const 25 000000000
+1010 concat 87 1009 1008
+1011 const 25 100000000
+1012 eq 1 86 1011
+1013 ite 87 1012 1010 1006
+1014 uext 87 1013 0 uut.txrx.encode_1.encoder.en8b10b.dataout
+1015 uext 87 1006 0 uut.txrx.encode_1.encoder.en8b10b.dataout_t
+1016 uext 1 903 0 uut.txrx.encode_1.encoder.en8b10b.dispin
+1017 or 1 976 965
+1018 xor 1 983 1017
+1019 uext 1 1018 0 uut.txrx.encode_1.encoder.en8b10b.dispout
+1020 uext 1 884 0 uut.txrx.encode_1.encoder.en8b10b.encoder.aeqb
+1021 uext 1 862 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ai
+1022 uext 1 971 0 uut.txrx.encode_1.encoder.en8b10b.encoder.alt7
+1023 uext 1 862 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ao
+1024 uext 1 869 0 uut.txrx.encode_1.encoder.en8b10b.encoder.bi
+1025 uext 1 930 0 uut.txrx.encode_1.encoder.en8b10b.encoder.bo
+1026 uext 1 887 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ceqd
+1027 uext 1 866 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ci
+1028 uext 1 933 0 uut.txrx.encode_1.encoder.en8b10b.encoder.co
+1029 uext 1 987 0 uut.txrx.encode_1.encoder.en8b10b.encoder.compls4
+1030 uext 1 922 0 uut.txrx.encode_1.encoder.en8b10b.encoder.compls6
+1031 uext 25 86 0 uut.txrx.encode_1.encoder.en8b10b.encoder.datain
+1032 uext 87 1006 0 uut.txrx.encode_1.encoder.en8b10b.encoder.dataout
+1033 uext 1 864 0 uut.txrx.encode_1.encoder.en8b10b.encoder.di
+1034 uext 1 983 0 uut.txrx.encode_1.encoder.en8b10b.encoder.disp6
+1035 uext 1 903 0 uut.txrx.encode_1.encoder.en8b10b.encoder.dispin
+1036 uext 1 1018 0 uut.txrx.encode_1.encoder.en8b10b.encoder.dispout
+1037 uext 1 936 0 uut.txrx.encode_1.encoder.en8b10b.encoder.do
+1038 uext 1 863 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ei
+1039 uext 1 940 0 uut.txrx.encode_1.encoder.en8b10b.encoder.eo
+1040 uext 1 961 0 uut.txrx.encode_1.encoder.en8b10b.encoder.fi
+1041 uext 1 973 0 uut.txrx.encode_1.encoder.en8b10b.encoder.fo
+1042 uext 1 962 0 uut.txrx.encode_1.encoder.en8b10b.encoder.gi
+1043 uext 1 991 0 uut.txrx.encode_1.encoder.en8b10b.encoder.go
+1044 uext 1 964 0 uut.txrx.encode_1.encoder.en8b10b.encoder.hi
+1045 uext 1 964 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ho
+1046 uext 1 959 0 uut.txrx.encode_1.encoder.en8b10b.encoder.io
+1047 uext 1 996 0 uut.txrx.encode_1.encoder.en8b10b.encoder.jo
+1048 uext 1 906 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ki
+1049 uext 1 929 0 uut.txrx.encode_1.encoder.en8b10b.encoder.l04
+1050 uext 1 912 0 uut.txrx.encode_1.encoder.en8b10b.encoder.l13
+1051 uext 1 890 0 uut.txrx.encode_1.encoder.en8b10b.encoder.l22
+1052 uext 1 897 0 uut.txrx.encode_1.encoder.en8b10b.encoder.l31
+1053 uext 1 925 0 uut.txrx.encode_1.encoder.en8b10b.encoder.l40
+1054 uext 1 963 0 uut.txrx.encode_1.encoder.en8b10b.encoder.nd1s4
+1055 uext 1 920 0 uut.txrx.encode_1.encoder.en8b10b.encoder.nd1s6
+1056 uext 1 976 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ndos4
+1057 uext 1 900 0 uut.txrx.encode_1.encoder.en8b10b.encoder.ndos6
+1058 uext 1 981 0 uut.txrx.encode_1.encoder.en8b10b.encoder.pd1s4
+1059 uext 1 900 0 uut.txrx.encode_1.encoder.en8b10b.encoder.pd1s6
+1060 uext 1 965 0 uut.txrx.encode_1.encoder.en8b10b.encoder.pdos4
+1061 uext 1 915 0 uut.txrx.encode_1.encoder.en8b10b.encoder.pdos6
+1062 state 1 uut.txrx.encode_1.encoder.lastbit
+1063 init 1 1062 9
+1064 const 260 001
+1065 state 260 uut.txrx.encode_1.encoder.max_counter
+1066 init 260 1065 1064
+1067 uext 1 1018 0 uut.txrx.encode_1.encoder.next_send_disp
+1068 uext 87 1013 0 uut.txrx.encode_1.encoder.send_bits
+1069 uext 1 75 0 uut.txrx.encode_1.encoder.send_valid
+1070 uext 25 86 0 uut.txrx.encode_1.encoder.send_word
+1071 state 1 uut.txrx.encode_1.encoder.stage2_bits
+1072 state 1 uut.txrx.encode_1.encoder.stage2_enable
+1073 state 1 uut.txrx.encode_1.encoder.stage2_shift
+1074 state 260 uut.txrx.hd_recv_wait
+1075 state 57 uut.txrx.hd_send_wait
+1076 state 1 uut.txrx.hd_switch_to_recv
+1077 state 1 uut.txrx.hd_switch_to_send
+1078 state 53 uut.txrx.ichecksum
+1079 state 25 uut.txrx.in_fifo_buffer[0]
+1080 state 25 uut.txrx.in_fifo_buffer[100]
+1081 state 25 uut.txrx.in_fifo_buffer[101]
+1082 state 25 uut.txrx.in_fifo_buffer[102]
+1083 state 25 uut.txrx.in_fifo_buffer[103]
+1084 state 25 uut.txrx.in_fifo_buffer[104]
+1085 state 25 uut.txrx.in_fifo_buffer[105]
+1086 state 25 uut.txrx.in_fifo_buffer[106]
+1087 state 25 uut.txrx.in_fifo_buffer[107]
+1088 state 25 uut.txrx.in_fifo_buffer[108]
+1089 state 25 uut.txrx.in_fifo_buffer[109]
+1090 state 25 uut.txrx.in_fifo_buffer[10]
+1091 state 25 uut.txrx.in_fifo_buffer[110]
+1092 state 25 uut.txrx.in_fifo_buffer[111]
+1093 state 25 uut.txrx.in_fifo_buffer[112]
+1094 state 25 uut.txrx.in_fifo_buffer[113]
+1095 state 25 uut.txrx.in_fifo_buffer[114]
+1096 state 25 uut.txrx.in_fifo_buffer[115]
+1097 state 25 uut.txrx.in_fifo_buffer[116]
+1098 state 25 uut.txrx.in_fifo_buffer[117]
+1099 state 25 uut.txrx.in_fifo_buffer[118]
+1100 state 25 uut.txrx.in_fifo_buffer[119]
+1101 state 25 uut.txrx.in_fifo_buffer[11]
+1102 state 25 uut.txrx.in_fifo_buffer[120]
+1103 state 25 uut.txrx.in_fifo_buffer[121]
+1104 state 25 uut.txrx.in_fifo_buffer[122]
+1105 state 25 uut.txrx.in_fifo_buffer[123]
+1106 state 25 uut.txrx.in_fifo_buffer[124]
+1107 state 25 uut.txrx.in_fifo_buffer[125]
+1108 state 25 uut.txrx.in_fifo_buffer[126]
+1109 state 25 uut.txrx.in_fifo_buffer[127]
+1110 state 25 uut.txrx.in_fifo_buffer[128]
+1111 state 25 uut.txrx.in_fifo_buffer[129]
+1112 state 25 uut.txrx.in_fifo_buffer[12]
+1113 state 25 uut.txrx.in_fifo_buffer[130]
+1114 state 25 uut.txrx.in_fifo_buffer[131]
+1115 state 25 uut.txrx.in_fifo_buffer[132]
+1116 state 25 uut.txrx.in_fifo_buffer[133]
+1117 state 25 uut.txrx.in_fifo_buffer[134]
+1118 state 25 uut.txrx.in_fifo_buffer[135]
+1119 state 25 uut.txrx.in_fifo_buffer[136]
+1120 state 25 uut.txrx.in_fifo_buffer[137]
+1121 state 25 uut.txrx.in_fifo_buffer[138]
+1122 state 25 uut.txrx.in_fifo_buffer[139]
+1123 state 25 uut.txrx.in_fifo_buffer[13]
+1124 state 25 uut.txrx.in_fifo_buffer[140]
+1125 state 25 uut.txrx.in_fifo_buffer[141]
+1126 state 25 uut.txrx.in_fifo_buffer[142]
+1127 state 25 uut.txrx.in_fifo_buffer[143]
+1128 state 25 uut.txrx.in_fifo_buffer[144]
+1129 state 25 uut.txrx.in_fifo_buffer[145]
+1130 state 25 uut.txrx.in_fifo_buffer[146]
+1131 state 25 uut.txrx.in_fifo_buffer[147]
+1132 state 25 uut.txrx.in_fifo_buffer[148]
+1133 state 25 uut.txrx.in_fifo_buffer[149]
+1134 state 25 uut.txrx.in_fifo_buffer[14]
+1135 state 25 uut.txrx.in_fifo_buffer[150]
+1136 state 25 uut.txrx.in_fifo_buffer[151]
+1137 state 25 uut.txrx.in_fifo_buffer[152]
+1138 state 25 uut.txrx.in_fifo_buffer[153]
+1139 state 25 uut.txrx.in_fifo_buffer[154]
+1140 state 25 uut.txrx.in_fifo_buffer[155]
+1141 state 25 uut.txrx.in_fifo_buffer[156]
+1142 state 25 uut.txrx.in_fifo_buffer[157]
+1143 state 25 uut.txrx.in_fifo_buffer[158]
+1144 state 25 uut.txrx.in_fifo_buffer[159]
+1145 state 25 uut.txrx.in_fifo_buffer[15]
+1146 state 25 uut.txrx.in_fifo_buffer[160]
+1147 state 25 uut.txrx.in_fifo_buffer[161]
+1148 state 25 uut.txrx.in_fifo_buffer[162]
+1149 state 25 uut.txrx.in_fifo_buffer[163]
+1150 state 25 uut.txrx.in_fifo_buffer[164]
+1151 state 25 uut.txrx.in_fifo_buffer[165]
+1152 state 25 uut.txrx.in_fifo_buffer[166]
+1153 state 25 uut.txrx.in_fifo_buffer[167]
+1154 state 25 uut.txrx.in_fifo_buffer[168]
+1155 state 25 uut.txrx.in_fifo_buffer[169]
+1156 state 25 uut.txrx.in_fifo_buffer[16]
+1157 state 25 uut.txrx.in_fifo_buffer[170]
+1158 state 25 uut.txrx.in_fifo_buffer[171]
+1159 state 25 uut.txrx.in_fifo_buffer[172]
+1160 state 25 uut.txrx.in_fifo_buffer[173]
+1161 state 25 uut.txrx.in_fifo_buffer[174]
+1162 state 25 uut.txrx.in_fifo_buffer[175]
+1163 state 25 uut.txrx.in_fifo_buffer[176]
+1164 state 25 uut.txrx.in_fifo_buffer[177]
+1165 state 25 uut.txrx.in_fifo_buffer[178]
+1166 state 25 uut.txrx.in_fifo_buffer[179]
+1167 state 25 uut.txrx.in_fifo_buffer[17]
+1168 state 25 uut.txrx.in_fifo_buffer[180]
+1169 state 25 uut.txrx.in_fifo_buffer[181]
+1170 state 25 uut.txrx.in_fifo_buffer[182]
+1171 state 25 uut.txrx.in_fifo_buffer[183]
+1172 state 25 uut.txrx.in_fifo_buffer[184]
+1173 state 25 uut.txrx.in_fifo_buffer[185]
+1174 state 25 uut.txrx.in_fifo_buffer[186]
+1175 state 25 uut.txrx.in_fifo_buffer[187]
+1176 state 25 uut.txrx.in_fifo_buffer[188]
+1177 state 25 uut.txrx.in_fifo_buffer[189]
+1178 state 25 uut.txrx.in_fifo_buffer[18]
+1179 state 25 uut.txrx.in_fifo_buffer[190]
+1180 state 25 uut.txrx.in_fifo_buffer[191]
+1181 state 25 uut.txrx.in_fifo_buffer[192]
+1182 state 25 uut.txrx.in_fifo_buffer[193]
+1183 state 25 uut.txrx.in_fifo_buffer[194]
+1184 state 25 uut.txrx.in_fifo_buffer[195]
+1185 state 25 uut.txrx.in_fifo_buffer[196]
+1186 state 25 uut.txrx.in_fifo_buffer[197]
+1187 state 25 uut.txrx.in_fifo_buffer[198]
+1188 state 25 uut.txrx.in_fifo_buffer[199]
+1189 state 25 uut.txrx.in_fifo_buffer[19]
+1190 state 25 uut.txrx.in_fifo_buffer[1]
+1191 state 25 uut.txrx.in_fifo_buffer[200]
+1192 state 25 uut.txrx.in_fifo_buffer[201]
+1193 state 25 uut.txrx.in_fifo_buffer[202]
+1194 state 25 uut.txrx.in_fifo_buffer[203]
+1195 state 25 uut.txrx.in_fifo_buffer[204]
+1196 state 25 uut.txrx.in_fifo_buffer[205]
+1197 state 25 uut.txrx.in_fifo_buffer[206]
+1198 state 25 uut.txrx.in_fifo_buffer[207]
+1199 state 25 uut.txrx.in_fifo_buffer[208]
+1200 state 25 uut.txrx.in_fifo_buffer[209]
+1201 state 25 uut.txrx.in_fifo_buffer[20]
+1202 state 25 uut.txrx.in_fifo_buffer[210]
+1203 state 25 uut.txrx.in_fifo_buffer[211]
+1204 state 25 uut.txrx.in_fifo_buffer[212]
+1205 state 25 uut.txrx.in_fifo_buffer[213]
+1206 state 25 uut.txrx.in_fifo_buffer[214]
+1207 state 25 uut.txrx.in_fifo_buffer[215]
+1208 state 25 uut.txrx.in_fifo_buffer[216]
+1209 state 25 uut.txrx.in_fifo_buffer[217]
+1210 state 25 uut.txrx.in_fifo_buffer[218]
+1211 state 25 uut.txrx.in_fifo_buffer[219]
+1212 state 25 uut.txrx.in_fifo_buffer[21]
+1213 state 25 uut.txrx.in_fifo_buffer[220]
+1214 state 25 uut.txrx.in_fifo_buffer[221]
+1215 state 25 uut.txrx.in_fifo_buffer[222]
+1216 state 25 uut.txrx.in_fifo_buffer[223]
+1217 state 25 uut.txrx.in_fifo_buffer[224]
+1218 state 25 uut.txrx.in_fifo_buffer[225]
+1219 state 25 uut.txrx.in_fifo_buffer[226]
+1220 state 25 uut.txrx.in_fifo_buffer[227]
+1221 state 25 uut.txrx.in_fifo_buffer[228]
+1222 state 25 uut.txrx.in_fifo_buffer[229]
+1223 state 25 uut.txrx.in_fifo_buffer[22]
+1224 state 25 uut.txrx.in_fifo_buffer[230]
+1225 state 25 uut.txrx.in_fifo_buffer[231]
+1226 state 25 uut.txrx.in_fifo_buffer[232]
+1227 state 25 uut.txrx.in_fifo_buffer[233]
+1228 state 25 uut.txrx.in_fifo_buffer[234]
+1229 state 25 uut.txrx.in_fifo_buffer[235]
+1230 state 25 uut.txrx.in_fifo_buffer[236]
+1231 state 25 uut.txrx.in_fifo_buffer[237]
+1232 state 25 uut.txrx.in_fifo_buffer[238]
+1233 state 25 uut.txrx.in_fifo_buffer[239]
+1234 state 25 uut.txrx.in_fifo_buffer[23]
+1235 state 25 uut.txrx.in_fifo_buffer[240]
+1236 state 25 uut.txrx.in_fifo_buffer[241]
+1237 state 25 uut.txrx.in_fifo_buffer[242]
+1238 state 25 uut.txrx.in_fifo_buffer[243]
+1239 state 25 uut.txrx.in_fifo_buffer[244]
+1240 state 25 uut.txrx.in_fifo_buffer[245]
+1241 state 25 uut.txrx.in_fifo_buffer[246]
+1242 state 25 uut.txrx.in_fifo_buffer[247]
+1243 state 25 uut.txrx.in_fifo_buffer[248]
+1244 state 25 uut.txrx.in_fifo_buffer[249]
+1245 state 25 uut.txrx.in_fifo_buffer[24]
+1246 state 25 uut.txrx.in_fifo_buffer[250]
+1247 state 25 uut.txrx.in_fifo_buffer[251]
+1248 state 25 uut.txrx.in_fifo_buffer[252]
+1249 state 25 uut.txrx.in_fifo_buffer[253]
+1250 state 25 uut.txrx.in_fifo_buffer[254]
+1251 state 25 uut.txrx.in_fifo_buffer[255]
+1252 state 25 uut.txrx.in_fifo_buffer[25]
+1253 state 25 uut.txrx.in_fifo_buffer[26]
+1254 state 25 uut.txrx.in_fifo_buffer[27]
+1255 state 25 uut.txrx.in_fifo_buffer[28]
+1256 state 25 uut.txrx.in_fifo_buffer[29]
+1257 state 25 uut.txrx.in_fifo_buffer[2]
+1258 state 25 uut.txrx.in_fifo_buffer[30]
+1259 state 25 uut.txrx.in_fifo_buffer[31]
+1260 state 25 uut.txrx.in_fifo_buffer[32]
+1261 state 25 uut.txrx.in_fifo_buffer[33]
+1262 state 25 uut.txrx.in_fifo_buffer[34]
+1263 state 25 uut.txrx.in_fifo_buffer[35]
+1264 state 25 uut.txrx.in_fifo_buffer[36]
+1265 state 25 uut.txrx.in_fifo_buffer[37]
+1266 state 25 uut.txrx.in_fifo_buffer[38]
+1267 state 25 uut.txrx.in_fifo_buffer[39]
+1268 state 25 uut.txrx.in_fifo_buffer[3]
+1269 state 25 uut.txrx.in_fifo_buffer[40]
+1270 state 25 uut.txrx.in_fifo_buffer[41]
+1271 state 25 uut.txrx.in_fifo_buffer[42]
+1272 state 25 uut.txrx.in_fifo_buffer[43]
+1273 state 25 uut.txrx.in_fifo_buffer[44]
+1274 state 25 uut.txrx.in_fifo_buffer[45]
+1275 state 25 uut.txrx.in_fifo_buffer[46]
+1276 state 25 uut.txrx.in_fifo_buffer[47]
+1277 state 25 uut.txrx.in_fifo_buffer[48]
+1278 state 25 uut.txrx.in_fifo_buffer[49]
+1279 state 25 uut.txrx.in_fifo_buffer[4]
+1280 state 25 uut.txrx.in_fifo_buffer[50]
+1281 state 25 uut.txrx.in_fifo_buffer[51]
+1282 state 25 uut.txrx.in_fifo_buffer[52]
+1283 state 25 uut.txrx.in_fifo_buffer[53]
+1284 state 25 uut.txrx.in_fifo_buffer[54]
+1285 state 25 uut.txrx.in_fifo_buffer[55]
+1286 state 25 uut.txrx.in_fifo_buffer[56]
+1287 state 25 uut.txrx.in_fifo_buffer[57]
+1288 state 25 uut.txrx.in_fifo_buffer[58]
+1289 state 25 uut.txrx.in_fifo_buffer[59]
+1290 state 25 uut.txrx.in_fifo_buffer[5]
+1291 state 25 uut.txrx.in_fifo_buffer[60]
+1292 state 25 uut.txrx.in_fifo_buffer[61]
+1293 state 25 uut.txrx.in_fifo_buffer[62]
+1294 state 25 uut.txrx.in_fifo_buffer[63]
+1295 state 25 uut.txrx.in_fifo_buffer[64]
+1296 state 25 uut.txrx.in_fifo_buffer[65]
+1297 state 25 uut.txrx.in_fifo_buffer[66]
+1298 state 25 uut.txrx.in_fifo_buffer[67]
+1299 state 25 uut.txrx.in_fifo_buffer[68]
+1300 state 25 uut.txrx.in_fifo_buffer[69]
+1301 state 25 uut.txrx.in_fifo_buffer[6]
+1302 state 25 uut.txrx.in_fifo_buffer[70]
+1303 state 25 uut.txrx.in_fifo_buffer[71]
+1304 state 25 uut.txrx.in_fifo_buffer[72]
+1305 state 25 uut.txrx.in_fifo_buffer[73]
+1306 state 25 uut.txrx.in_fifo_buffer[74]
+1307 state 25 uut.txrx.in_fifo_buffer[75]
+1308 state 25 uut.txrx.in_fifo_buffer[76]
+1309 state 25 uut.txrx.in_fifo_buffer[77]
+1310 state 25 uut.txrx.in_fifo_buffer[78]
+1311 state 25 uut.txrx.in_fifo_buffer[79]
+1312 state 25 uut.txrx.in_fifo_buffer[7]
+1313 state 25 uut.txrx.in_fifo_buffer[80]
+1314 state 25 uut.txrx.in_fifo_buffer[81]
+1315 state 25 uut.txrx.in_fifo_buffer[82]
+1316 state 25 uut.txrx.in_fifo_buffer[83]
+1317 state 25 uut.txrx.in_fifo_buffer[84]
+1318 state 25 uut.txrx.in_fifo_buffer[85]
+1319 state 25 uut.txrx.in_fifo_buffer[86]
+1320 state 25 uut.txrx.in_fifo_buffer[87]
+1321 state 25 uut.txrx.in_fifo_buffer[88]
+1322 state 25 uut.txrx.in_fifo_buffer[89]
+1323 state 25 uut.txrx.in_fifo_buffer[8]
+1324 state 25 uut.txrx.in_fifo_buffer[90]
+1325 state 25 uut.txrx.in_fifo_buffer[91]
+1326 state 25 uut.txrx.in_fifo_buffer[92]
+1327 state 25 uut.txrx.in_fifo_buffer[93]
+1328 state 25 uut.txrx.in_fifo_buffer[94]
+1329 state 25 uut.txrx.in_fifo_buffer[95]
+1330 state 25 uut.txrx.in_fifo_buffer[96]
+1331 state 25 uut.txrx.in_fifo_buffer[97]
+1332 state 25 uut.txrx.in_fifo_buffer[98]
+1333 state 25 uut.txrx.in_fifo_buffer[99]
+1334 state 25 uut.txrx.in_fifo_buffer[9]
+1335 uext 28 32 0 uut.txrx.in_fifo_iptr_nxt
+1336 uext 28 33 0 uut.txrx.in_fifo_oblock
+1337 state 28 uut.txrx.in_fifo_optr
+1338 uext 28 30 7
+1339 add 28 1337 1338
+1340 uext 28 1339 0 uut.txrx.in_fifo_optr_nxt
+1341 uext 25 26 0 uut.txrx.in_ser_tdata
+1342 uext 1 35 0 uut.txrx.in_ser_tready
+1343 uext 1 37 0 uut.txrx.in_ser_tvalid
+1344 state 17 uut.txrx.istate
+1345 state 28 uut.txrx.next_sent_gpio
+1346 state 28 uut.txrx.next_sent_gpio_at
+1347 state 17 uut.txrx.ostate
+1348 state 266 uut.txrx.ostate_counter
+1349 state 1 uut.txrx.ostate_reset
+1350 uext 28 30 7
+1351 add 28 43 1350
+1352 uext 28 1351 0 uut.txrx.out_fifo_optr_nxt
+1353 uext 1 40 0 uut.txrx.out_ser_tready
+1354 uext 1 45 0 uut.txrx.out_ser_tvalid
+1355 state 28 uut.txrx.peer_out_fifo_iptr_next
+1356 uext 1 842 0 uut.txrx.recv_error
+1357 uext 25 269 0 uut.txrx.recv_word
+1358 uext 1 82 0 uut.txrx.recv_word_en
+1359 uext 1 20 0 uut.txrx.resetn_out
+1360 uext 1 846 0 uut.txrx.rstdetect
+1361 uext 1 77 0 uut.txrx.send_ready
+1362 state 25 uut.txrx.sent_gpio
+1363 uext 1 63 0 uut.txrx.serdes_en
+1364 uext 1 66 0 uut.txrx.serdes_in
+1365 uext 1 69 0 uut.txrx.serdes_out
+1366 state 28 uut.txrx.work_out_fifo_iptr
+1367 state 1 uut.txrx.work_out_fifo_iptr_apply
+1368 uext 28 30 7
+1369 add 28 1366 1368
+1370 uext 28 1369 0 uut.txrx.work_out_fifo_iptr_nxt
+1371 uext 1 2 0 uut.unpack_8bits.unpacker.clk
+1372 uext 1 20 0 uut.unpack_8bits.unpacker.resetn
+1373 uext 1 45 0 uut.unpack_8bits.unpacker.ser_tvalid
+1374 sort bitvec 228
+1375 const 1374 000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
+1376 state 1374 xfer_shreg
+1377 init 1374 1376 1375
+1378 next 1 4 63
+1379 next 1 6 69
+1380 slice 1 1376 227 227
+1381 slice 1 1376 226 226
+1382 concat 258 1381 1380
+1383 slice 1 1376 225 225
+1384 concat 260 1383 1382
+1385 slice 1 1376 224 224
+1386 concat 17 1385 1384
+1387 slice 1 1376 223 223
+1388 concat 57 1387 1386
+1389 slice 1 1376 222 222
+1390 concat 264 1389 1388
+1391 slice 1 1376 221 221
+1392 concat 266 1391 1390
+1393 slice 1 1376 220 220
+1394 concat 28 1393 1392
+1395 slice 1 1376 219 219
+1396 concat 25 1395 1394
+1397 slice 1 1376 218 218
+1398 concat 87 1397 1396
+1399 slice 1 1376 217 217
+1400 concat 545 1399 1398
+1401 slice 1 1376 216 216
+1402 concat 55 1401 1400
+1403 slice 1 1376 215 215
+1404 concat 548 1403 1402
+1405 slice 1 1376 214 214
+1406 concat 550 1405 1404
+1407 slice 1 1376 213 213
+1408 concat 552 1407 1406
+1409 slice 1 1376 212 212
+1410 concat 554 1409 1408
+1411 slice 1 1376 211 211
+1412 concat 556 1411 1410
+1413 slice 1 1376 210 210
+1414 concat 558 1413 1412
+1415 slice 1 1376 209 209
+1416 concat 560 1415 1414
+1417 slice 1 1376 208 208
+1418 concat 562 1417 1416
+1419 slice 1 1376 207 207
+1420 concat 564 1419 1418
+1421 slice 1 1376 206 206
+1422 concat 566 1421 1420
+1423 slice 1 1376 205 205
+1424 concat 568 1423 1422
+1425 slice 1 1376 204 204
+1426 concat 570 1425 1424
+1427 slice 1 1376 203 203
+1428 concat 572 1427 1426
+1429 slice 1 1376 202 202
+1430 concat 574 1429 1428
+1431 slice 1 1376 201 201
+1432 concat 576 1431 1430
+1433 slice 1 1376 200 200
+1434 concat 578 1433 1432
+1435 slice 1 1376 199 199
+1436 concat 580 1435 1434
+1437 slice 1 1376 198 198
+1438 concat 582 1437 1436
+1439 slice 1 1376 197 197
+1440 concat 584 1439 1438
+1441 slice 1 1376 196 196
+1442 concat 53 1441 1440
+1443 slice 1 1376 195 195
+1444 sort bitvec 33
+1445 concat 1444 1443 1442
+1446 slice 1 1376 194 194
+1447 sort bitvec 34
+1448 concat 1447 1446 1445
+1449 slice 1 1376 193 193
+1450 sort bitvec 35
+1451 concat 1450 1449 1448
+1452 slice 1 1376 192 192
+1453 sort bitvec 36
+1454 concat 1453 1452 1451
+1455 slice 1 1376 191 191
+1456 sort bitvec 37
+1457 concat 1456 1455 1454
+1458 slice 1 1376 190 190
+1459 sort bitvec 38
+1460 concat 1459 1458 1457
+1461 slice 1 1376 189 189
+1462 sort bitvec 39
+1463 concat 1462 1461 1460
+1464 slice 1 1376 188 188
+1465 sort bitvec 40
+1466 concat 1465 1464 1463
+1467 slice 1 1376 187 187
+1468 sort bitvec 41
+1469 concat 1468 1467 1466
+1470 slice 1 1376 186 186
+1471 sort bitvec 42
+1472 concat 1471 1470 1469
+1473 slice 1 1376 185 185
+1474 sort bitvec 43
+1475 concat 1474 1473 1472
+1476 slice 1 1376 184 184
+1477 sort bitvec 44
+1478 concat 1477 1476 1475
+1479 slice 1 1376 183 183
+1480 sort bitvec 45
+1481 concat 1480 1479 1478
+1482 slice 1 1376 182 182
+1483 sort bitvec 46
+1484 concat 1483 1482 1481
+1485 slice 1 1376 181 181
+1486 sort bitvec 47
+1487 concat 1486 1485 1484
+1488 slice 1 1376 180 180
+1489 sort bitvec 48
+1490 concat 1489 1488 1487
+1491 slice 1 1376 179 179
+1492 sort bitvec 49
+1493 concat 1492 1491 1490
+1494 slice 1 1376 178 178
+1495 sort bitvec 50
+1496 concat 1495 1494 1493
+1497 slice 1 1376 177 177
+1498 sort bitvec 51
+1499 concat 1498 1497 1496
+1500 slice 1 1376 176 176
+1501 sort bitvec 52
+1502 concat 1501 1500 1499
+1503 slice 1 1376 175 175
+1504 sort bitvec 53
+1505 concat 1504 1503 1502
+1506 slice 1 1376 174 174
+1507 sort bitvec 54
+1508 concat 1507 1506 1505
+1509 slice 1 1376 173 173
+1510 sort bitvec 55
+1511 concat 1510 1509 1508
+1512 slice 1 1376 172 172
+1513 sort bitvec 56
+1514 concat 1513 1512 1511
+1515 slice 1 1376 171 171
+1516 sort bitvec 57
+1517 concat 1516 1515 1514
+1518 slice 1 1376 170 170
+1519 sort bitvec 58
+1520 concat 1519 1518 1517
+1521 slice 1 1376 169 169
+1522 sort bitvec 59
+1523 concat 1522 1521 1520
+1524 slice 1 1376 168 168
+1525 sort bitvec 60
+1526 concat 1525 1524 1523
+1527 slice 1 1376 167 167
+1528 sort bitvec 61
+1529 concat 1528 1527 1526
+1530 slice 1 1376 166 166
+1531 sort bitvec 62
+1532 concat 1531 1530 1529
+1533 slice 1 1376 165 165
+1534 sort bitvec 63
+1535 concat 1534 1533 1532
+1536 slice 1 1376 164 164
+1537 sort bitvec 64
+1538 concat 1537 1536 1535
+1539 slice 1 1376 163 163
+1540 sort bitvec 65
+1541 concat 1540 1539 1538
+1542 slice 1 1376 162 162
+1543 sort bitvec 66
+1544 concat 1543 1542 1541
+1545 slice 1 1376 161 161
+1546 sort bitvec 67
+1547 concat 1546 1545 1544
+1548 slice 1 1376 160 160
+1549 sort bitvec 68
+1550 concat 1549 1548 1547
+1551 slice 1 1376 159 159
+1552 sort bitvec 69
+1553 concat 1552 1551 1550
+1554 slice 1 1376 158 158
+1555 sort bitvec 70
+1556 concat 1555 1554 1553
+1557 slice 1 1376 157 157
+1558 sort bitvec 71
+1559 concat 1558 1557 1556
+1560 slice 1 1376 156 156
+1561 sort bitvec 72
+1562 concat 1561 1560 1559
+1563 slice 1 1376 155 155
+1564 sort bitvec 73
+1565 concat 1564 1563 1562
+1566 slice 1 1376 154 154
+1567 sort bitvec 74
+1568 concat 1567 1566 1565
+1569 slice 1 1376 153 153
+1570 sort bitvec 75
+1571 concat 1570 1569 1568
+1572 slice 1 1376 152 152
+1573 sort bitvec 76
+1574 concat 1573 1572 1571
+1575 slice 1 1376 151 151
+1576 sort bitvec 77
+1577 concat 1576 1575 1574
+1578 slice 1 1376 150 150
+1579 sort bitvec 78
+1580 concat 1579 1578 1577
+1581 slice 1 1376 149 149
+1582 sort bitvec 79
+1583 concat 1582 1581 1580
+1584 slice 1 1376 148 148
+1585 sort bitvec 80
+1586 concat 1585 1584 1583
+1587 slice 1 1376 147 147
+1588 sort bitvec 81
+1589 concat 1588 1587 1586
+1590 slice 1 1376 146 146
+1591 sort bitvec 82
+1592 concat 1591 1590 1589
+1593 slice 1 1376 145 145
+1594 sort bitvec 83
+1595 concat 1594 1593 1592
+1596 slice 1 1376 144 144
+1597 sort bitvec 84
+1598 concat 1597 1596 1595
+1599 slice 1 1376 143 143
+1600 sort bitvec 85
+1601 concat 1600 1599 1598
+1602 slice 1 1376 142 142
+1603 sort bitvec 86
+1604 concat 1603 1602 1601
+1605 slice 1 1376 141 141
+1606 sort bitvec 87
+1607 concat 1606 1605 1604
+1608 slice 1 1376 140 140
+1609 sort bitvec 88
+1610 concat 1609 1608 1607
+1611 slice 1 1376 139 139
+1612 sort bitvec 89
+1613 concat 1612 1611 1610
+1614 slice 1 1376 138 138
+1615 sort bitvec 90
+1616 concat 1615 1614 1613
+1617 slice 1 1376 137 137
+1618 sort bitvec 91
+1619 concat 1618 1617 1616
+1620 slice 1 1376 136 136
+1621 sort bitvec 92
+1622 concat 1621 1620 1619
+1623 slice 1 1376 135 135
+1624 sort bitvec 93
+1625 concat 1624 1623 1622
+1626 slice 1 1376 134 134
+1627 sort bitvec 94
+1628 concat 1627 1626 1625
+1629 slice 1 1376 133 133
+1630 sort bitvec 95
+1631 concat 1630 1629 1628
+1632 slice 1 1376 132 132
+1633 sort bitvec 96
+1634 concat 1633 1632 1631
+1635 slice 1 1376 131 131
+1636 sort bitvec 97
+1637 concat 1636 1635 1634
+1638 slice 1 1376 130 130
+1639 sort bitvec 98
+1640 concat 1639 1638 1637
+1641 slice 1 1376 129 129
+1642 sort bitvec 99
+1643 concat 1642 1641 1640
+1644 slice 1 1376 128 128
+1645 sort bitvec 100
+1646 concat 1645 1644 1643
+1647 slice 1 1376 127 127
+1648 sort bitvec 101
+1649 concat 1648 1647 1646
+1650 slice 1 1376 126 126
+1651 sort bitvec 102
+1652 concat 1651 1650 1649
+1653 slice 1 1376 125 125
+1654 sort bitvec 103
+1655 concat 1654 1653 1652
+1656 slice 1 1376 124 124
+1657 sort bitvec 104
+1658 concat 1657 1656 1655
+1659 slice 1 1376 123 123
+1660 sort bitvec 105
+1661 concat 1660 1659 1658
+1662 slice 1 1376 122 122
+1663 sort bitvec 106
+1664 concat 1663 1662 1661
+1665 slice 1 1376 121 121
+1666 sort bitvec 107
+1667 concat 1666 1665 1664
+1668 slice 1 1376 120 120
+1669 sort bitvec 108
+1670 concat 1669 1668 1667
+1671 slice 1 1376 119 119
+1672 sort bitvec 109
+1673 concat 1672 1671 1670
+1674 slice 1 1376 118 118
+1675 sort bitvec 110
+1676 concat 1675 1674 1673
+1677 slice 1 1376 117 117
+1678 sort bitvec 111
+1679 concat 1678 1677 1676
+1680 slice 1 1376 116 116
+1681 sort bitvec 112
+1682 concat 1681 1680 1679
+1683 slice 1 1376 115 115
+1684 sort bitvec 113
+1685 concat 1684 1683 1682
+1686 slice 1 1376 114 114
+1687 sort bitvec 114
+1688 concat 1687 1686 1685
+1689 slice 1 1376 113 113
+1690 sort bitvec 115
+1691 concat 1690 1689 1688
+1692 slice 1 1376 112 112
+1693 sort bitvec 116
+1694 concat 1693 1692 1691
+1695 slice 1 1376 111 111
+1696 sort bitvec 117
+1697 concat 1696 1695 1694
+1698 slice 1 1376 110 110
+1699 sort bitvec 118
+1700 concat 1699 1698 1697
+1701 slice 1 1376 109 109
+1702 sort bitvec 119
+1703 concat 1702 1701 1700
+1704 slice 1 1376 108 108
+1705 sort bitvec 120
+1706 concat 1705 1704 1703
+1707 slice 1 1376 107 107
+1708 sort bitvec 121
+1709 concat 1708 1707 1706
+1710 slice 1 1376 106 106
+1711 sort bitvec 122
+1712 concat 1711 1710 1709
+1713 slice 1 1376 105 105
+1714 sort bitvec 123
+1715 concat 1714 1713 1712
+1716 slice 1 1376 104 104
+1717 sort bitvec 124
+1718 concat 1717 1716 1715
+1719 slice 1 1376 103 103
+1720 sort bitvec 125
+1721 concat 1720 1719 1718
+1722 slice 1 1376 102 102
+1723 sort bitvec 126
+1724 concat 1723 1722 1721
+1725 slice 1 1376 101 101
+1726 sort bitvec 127
+1727 concat 1726 1725 1724
+1728 slice 1 1376 100 100
+1729 sort bitvec 128
+1730 concat 1729 1728 1727
+1731 slice 1 1376 99 99
+1732 sort bitvec 129
+1733 concat 1732 1731 1730
+1734 slice 1 1376 98 98
+1735 sort bitvec 130
+1736 concat 1735 1734 1733
+1737 slice 1 1376 97 97
+1738 sort bitvec 131
+1739 concat 1738 1737 1736
+1740 slice 1 1376 96 96
+1741 sort bitvec 132
+1742 concat 1741 1740 1739
+1743 slice 1 1376 95 95
+1744 sort bitvec 133
+1745 concat 1744 1743 1742
+1746 slice 1 1376 94 94
+1747 sort bitvec 134
+1748 concat 1747 1746 1745
+1749 slice 1 1376 93 93
+1750 sort bitvec 135
+1751 concat 1750 1749 1748
+1752 slice 1 1376 92 92
+1753 sort bitvec 136
+1754 concat 1753 1752 1751
+1755 slice 1 1376 91 91
+1756 sort bitvec 137
+1757 concat 1756 1755 1754
+1758 slice 1 1376 90 90
+1759 sort bitvec 138
+1760 concat 1759 1758 1757
+1761 slice 1 1376 89 89
+1762 sort bitvec 139
+1763 concat 1762 1761 1760
+1764 slice 1 1376 88 88
+1765 sort bitvec 140
+1766 concat 1765 1764 1763
+1767 slice 1 1376 87 87
+1768 sort bitvec 141
+1769 concat 1768 1767 1766
+1770 slice 1 1376 86 86
+1771 sort bitvec 142
+1772 concat 1771 1770 1769
+1773 slice 1 1376 85 85
+1774 sort bitvec 143
+1775 concat 1774 1773 1772
+1776 slice 1 1376 84 84
+1777 sort bitvec 144
+1778 concat 1777 1776 1775
+1779 slice 1 1376 83 83
+1780 sort bitvec 145
+1781 concat 1780 1779 1778
+1782 slice 1 1376 82 82
+1783 sort bitvec 146
+1784 concat 1783 1782 1781
+1785 slice 1 1376 81 81
+1786 sort bitvec 147
+1787 concat 1786 1785 1784
+1788 slice 1 1376 80 80
+1789 sort bitvec 148
+1790 concat 1789 1788 1787
+1791 slice 1 1376 79 79
+1792 sort bitvec 149
+1793 concat 1792 1791 1790
+1794 slice 1 1376 78 78
+1795 sort bitvec 150
+1796 concat 1795 1794 1793
+1797 slice 1 1376 77 77
+1798 sort bitvec 151
+1799 concat 1798 1797 1796
+1800 slice 1 1376 76 76
+1801 sort bitvec 152
+1802 concat 1801 1800 1799
+1803 slice 1 1376 75 75
+1804 sort bitvec 153
+1805 concat 1804 1803 1802
+1806 slice 1 1376 74 74
+1807 sort bitvec 154
+1808 concat 1807 1806 1805
+1809 slice 1 1376 73 73
+1810 sort bitvec 155
+1811 concat 1810 1809 1808
+1812 slice 1 1376 72 72
+1813 sort bitvec 156
+1814 concat 1813 1812 1811
+1815 slice 1 1376 71 71
+1816 sort bitvec 157
+1817 concat 1816 1815 1814
+1818 slice 1 1376 70 70
+1819 sort bitvec 158
+1820 concat 1819 1818 1817
+1821 slice 1 1376 69 69
+1822 sort bitvec 159
+1823 concat 1822 1821 1820
+1824 slice 1 1376 68 68
+1825 sort bitvec 160
+1826 concat 1825 1824 1823
+1827 slice 1 1376 67 67
+1828 sort bitvec 161
+1829 concat 1828 1827 1826
+1830 slice 1 1376 66 66
+1831 sort bitvec 162
+1832 concat 1831 1830 1829
+1833 slice 1 1376 65 65
+1834 sort bitvec 163
+1835 concat 1834 1833 1832
+1836 slice 1 1376 64 64
+1837 sort bitvec 164
+1838 concat 1837 1836 1835
+1839 slice 1 1376 63 63
+1840 sort bitvec 165
+1841 concat 1840 1839 1838
+1842 slice 1 1376 62 62
+1843 sort bitvec 166
+1844 concat 1843 1842 1841
+1845 slice 1 1376 61 61
+1846 sort bitvec 167
+1847 concat 1846 1845 1844
+1848 slice 1 1376 60 60
+1849 sort bitvec 168
+1850 concat 1849 1848 1847
+1851 slice 1 1376 59 59
+1852 sort bitvec 169
+1853 concat 1852 1851 1850
+1854 slice 1 1376 58 58
+1855 sort bitvec 170
+1856 concat 1855 1854 1853
+1857 slice 1 1376 57 57
+1858 sort bitvec 171
+1859 concat 1858 1857 1856
+1860 slice 1 1376 56 56
+1861 sort bitvec 172
+1862 concat 1861 1860 1859
+1863 slice 1 1376 55 55
+1864 sort bitvec 173
+1865 concat 1864 1863 1862
+1866 slice 1 1376 54 54
+1867 sort bitvec 174
+1868 concat 1867 1866 1865
+1869 slice 1 1376 53 53
+1870 sort bitvec 175
+1871 concat 1870 1869 1868
+1872 slice 1 1376 52 52
+1873 sort bitvec 176
+1874 concat 1873 1872 1871
+1875 slice 1 1376 51 51
+1876 sort bitvec 177
+1877 concat 1876 1875 1874
+1878 slice 1 1376 50 50
+1879 sort bitvec 178
+1880 concat 1879 1878 1877
+1881 slice 1 1376 49 49
+1882 sort bitvec 179
+1883 concat 1882 1881 1880
+1884 slice 1 1376 48 48
+1885 sort bitvec 180
+1886 concat 1885 1884 1883
+1887 slice 1 1376 47 47
+1888 sort bitvec 181
+1889 concat 1888 1887 1886
+1890 slice 1 1376 46 46
+1891 sort bitvec 182
+1892 concat 1891 1890 1889
+1893 slice 1 1376 45 45
+1894 sort bitvec 183
+1895 concat 1894 1893 1892
+1896 slice 1 1376 44 44
+1897 sort bitvec 184
+1898 concat 1897 1896 1895
+1899 slice 1 1376 43 43
+1900 sort bitvec 185
+1901 concat 1900 1899 1898
+1902 slice 1 1376 42 42
+1903 sort bitvec 186
+1904 concat 1903 1902 1901
+1905 slice 1 1376 41 41
+1906 sort bitvec 187
+1907 concat 1906 1905 1904
+1908 slice 1 1376 40 40
+1909 sort bitvec 188
+1910 concat 1909 1908 1907
+1911 slice 1 1376 39 39
+1912 sort bitvec 189
+1913 concat 1912 1911 1910
+1914 slice 1 1376 38 38
+1915 sort bitvec 190
+1916 concat 1915 1914 1913
+1917 slice 1 1376 37 37
+1918 sort bitvec 191
+1919 concat 1918 1917 1916
+1920 slice 1 1376 36 36
+1921 sort bitvec 192
+1922 concat 1921 1920 1919
+1923 slice 1 1376 35 35
+1924 sort bitvec 193
+1925 concat 1924 1923 1922
+1926 slice 1 1376 34 34
+1927 sort bitvec 194
+1928 concat 1927 1926 1925
+1929 slice 1 1376 33 33
+1930 sort bitvec 195
+1931 concat 1930 1929 1928
+1932 slice 1 1376 32 32
+1933 sort bitvec 196
+1934 concat 1933 1932 1931
+1935 slice 1 1376 31 31
+1936 sort bitvec 197
+1937 concat 1936 1935 1934
+1938 slice 1 1376 30 30
+1939 sort bitvec 198
+1940 concat 1939 1938 1937
+1941 slice 1 1376 29 29
+1942 sort bitvec 199
+1943 concat 1942 1941 1940
+1944 slice 1 1376 28 28
+1945 sort bitvec 200
+1946 concat 1945 1944 1943
+1947 slice 1 1376 27 27
+1948 sort bitvec 201
+1949 concat 1948 1947 1946
+1950 slice 1 1376 26 26
+1951 sort bitvec 202
+1952 concat 1951 1950 1949
+1953 slice 1 1376 25 25
+1954 sort bitvec 203
+1955 concat 1954 1953 1952
+1956 slice 1 1376 24 24
+1957 sort bitvec 204
+1958 concat 1957 1956 1955
+1959 slice 1 1376 23 23
+1960 sort bitvec 205
+1961 concat 1960 1959 1958
+1962 slice 1 1376 22 22
+1963 sort bitvec 206
+1964 concat 1963 1962 1961
+1965 slice 1 1376 21 21
+1966 sort bitvec 207
+1967 concat 1966 1965 1964
+1968 slice 1 1376 20 20
+1969 sort bitvec 208
+1970 concat 1969 1968 1967
+1971 slice 1 1376 19 19
+1972 sort bitvec 209
+1973 concat 1972 1971 1970
+1974 slice 1 1376 18 18
+1975 sort bitvec 210
+1976 concat 1975 1974 1973
+1977 slice 1 1376 17 17
+1978 sort bitvec 211
+1979 concat 1978 1977 1976
+1980 slice 1 1376 16 16
+1981 sort bitvec 212
+1982 concat 1981 1980 1979
+1983 slice 1 1376 15 15
+1984 sort bitvec 213
+1985 concat 1984 1983 1982
+1986 slice 1 1376 14 14
+1987 sort bitvec 214
+1988 concat 1987 1986 1985
+1989 slice 1 1376 13 13
+1990 sort bitvec 215
+1991 concat 1990 1989 1988
+1992 slice 1 1376 12 12
+1993 sort bitvec 216
+1994 concat 1993 1992 1991
+1995 slice 1 1376 11 11
+1996 sort bitvec 217
+1997 concat 1996 1995 1994
+1998 slice 1 1376 10 10
+1999 sort bitvec 218
+2000 concat 1999 1998 1997
+2001 slice 1 1376 9 9
+2002 sort bitvec 219
+2003 concat 2002 2001 2000
+2004 slice 1 1376 8 8
+2005 sort bitvec 220
+2006 concat 2005 2004 2003
+2007 slice 1 1376 7 7
+2008 sort bitvec 221
+2009 concat 2008 2007 2006
+2010 slice 1 1376 6 6
+2011 sort bitvec 222
+2012 concat 2011 2010 2009
+2013 slice 1 1376 5 5
+2014 sort bitvec 223
+2015 concat 2014 2013 2012
+2016 slice 1 1376 4 4
+2017 sort bitvec 224
+2018 concat 2017 2016 2015
+2019 slice 1 1376 3 3
+2020 sort bitvec 225
+2021 concat 2020 2019 2018
+2022 slice 1 1376 2 2
+2023 sort bitvec 226
+2024 concat 2023 2022 2021
+2025 slice 1 1376 1 1
+2026 sort bitvec 227
+2027 concat 2026 2025 2024
+2028 slice 1 1376 0 0
+2029 concat 1374 2028 2027
+2030 redand 1 2029
+2031 not 1 2030
+2032 next 1 8 2031
+2033 next 1 10 30
+2034 ite 1 21 30 15
+2035 ite 1 15 9 2034
+2036 ite 1 49 2034 2035
+2037 or 1 49 15
+2038 ite 1 2037 2036 2034
+2039 ite 1 48 2034 2038
+2040 ite 1 50 2034 2039
+2041 redor 1 58
+2042 ite 1 2041 2034 2040
+2043 not 1 37
+2044 or 1 2043 35
+2045 ite 1 2044 2042 2034
+2046 ite 1 20 2045 9
+2047 next 1 15 2046
+2048 uext 17 30 3
+2049 sub 17 18 2048
+2050 redor 1 18
+2051 ite 17 2050 2049 18
+2052 const 17 1111
+2053 const 53 00000000000000000000000000000001
+2054 redor 1 2053
+2055 and 1 2054 846
+2056 ite 17 2055 2052 2051
+2057 next 17 18 2056
+2058 slice 28 54 7 0
+2059 concat 25 9 2058
+2060 ite 25 15 2059 26
+2061 slice 28 54 7 0
+2062 xor 28 51 2061
+2063 concat 25 9 2062
+2064 ite 25 49 2063 2060
+2065 ite 25 2037 2064 26
+2066 const 25 101011100
+2067 ite 25 48 2066 2065
+2068 const 25 101111100
+2069 ite 25 50 2068 2067
+2070 slice 28 54 31 24
+2071 concat 25 9 2070
+2072 slice 28 54 23 16
+2073 concat 25 9 2072
+2074 slice 1 58 3 3
+2075 ite 25 2074 2073 2071
+2076 slice 28 54 15 8
+2077 concat 25 9 2076
+2078 slice 1 58 2 2
+2079 ite 25 2078 2077 2075
+2080 slice 1 58 1 1
+2081 ite 25 2080 2059 2079
+2082 const 25 100011100
+2083 slice 1 58 0 0
+2084 ite 25 2083 2082 2081
+2085 ite 25 2041 2084 2069
+2086 ite 25 2044 2085 26
+2087 ite 25 20 2086 26
+2088 next 25 26 2087
+2089 const 28 00000000
+2090 and 1 37 35
+2091 ite 28 2090 32 29
+2092 ite 28 20 2091 2089
+2093 next 28 29 2092
+2094 slice 28 1078 31 24
+2095 uext 25 2094 1
+2096 eq 1 269 2095
+2097 ite 28 2096 1355 33
+2098 const 17 1010
+2099 eq 1 1344 2098
+2100 const 17 1001
+2101 eq 1 1344 2100
+2102 const 17 1000
+2103 eq 1 1344 2102
+2104 const 260 110
+2105 uext 17 2104 1
+2106 eq 1 1344 2105
+2107 const 260 100
+2108 uext 17 2107 1
+2109 eq 1 1344 2108
+2110 const 258 11
+2111 uext 17 2110 2
+2112 eq 1 1344 2111
+2113 const 258 10
+2114 uext 17 2113 2
+2115 eq 1 1344 2114
+2116 uext 17 30 3
+2117 eq 1 1344 2116
+2118 redor 1 1344
+2119 not 1 2118
+2120 concat 258 2101 2099
+2121 concat 260 2103 2120
+2122 concat 17 2106 2121
+2123 concat 57 2109 2122
+2124 concat 264 2112 2123
+2125 concat 266 2115 2124
+2126 concat 28 2117 2125
+2127 concat 25 2119 2126
+2128 redor 1 2127
+2129 ite 28 2128 33 2097
+2130 eq 1 269 588
+2131 ite 28 2130 33 2129
+2132 ite 28 842 33 2131
+2133 redor 1 1074
+2134 not 1 2133
+2135 and 1 82 2134
+2136 not 1 63
+2137 and 1 2135 2136
+2138 ite 28 2137 2132 33
+2139 ite 28 80 33 2138
+2140 ite 28 20 2139 2089
+2141 next 28 33 2140
+2142 ite 1 15 30 37
+2143 ite 1 49 30 2142
+2144 ite 1 2037 2143 9
+2145 ite 1 48 30 2144
+2146 ite 1 50 30 2145
+2147 ite 1 2041 30 2146
+2148 ite 1 2044 2147 37
+2149 ite 1 20 2148 9
+2150 next 1 37 2149
+2151 not 1 40
+2152 and 1 2151 45
+2153 ite 1 2152 30 9
+2154 ite 1 20 2153 9
+2155 next 1 40 2154
+2156 ite 28 1367 1366 42
+2157 ite 28 2096 2156 42
+2158 ite 28 2128 42 2157
+2159 ite 28 2130 42 2158
+2160 ite 28 842 42 2159
+2161 ite 28 2137 2160 42
+2162 ite 28 80 42 2161
+2163 ite 28 20 2162 2089
+2164 next 28 42 2163
+2165 and 1 45 40
+2166 ite 28 2165 1351 43
+2167 ite 28 20 2166 2089
+2168 next 28 43 2167
+2169 uext 28 9 7
+2170 neq 1 51 2169
+2171 ite 1 21 2170 48
+2172 ite 1 48 9 2171
+2173 ite 1 50 2171 2172
+2174 ite 1 2041 2171 2173
+2175 ite 1 2044 2174 2171
+2176 ite 1 20 2175 9
+2177 next 1 48 2176
+2178 ite 1 21 9 49
+2179 ite 1 49 9 2178
+2180 ite 1 2037 2179 2178
+2181 ite 1 48 30 2180
+2182 ite 1 50 2178 2181
+2183 ite 1 2041 2178 2182
+2184 ite 1 2044 2183 2178
+2185 ite 1 20 2184 9
+2186 next 1 49 2185
+2187 ite 1 21 9 50
+2188 ite 1 50 9 2187
+2189 ite 1 2041 2187 2188
+2190 ite 1 2044 2189 2187
+2191 ite 1 20 2190 9
+2192 next 1 50 2191
+2193 ite 28 21 2089 51
+2194 ite 28 20 2193 2089
+2195 next 28 51 2194
+2196 const 53 00000111010110111100110100010101
+2197 const 548 0000000000000
+2198 slice 560 54 18 0
+2199 concat 53 2198 2197
+2200 xor 53 54 2199
+2201 slice 552 2200 31 17
+2202 uext 53 2201 17
+2203 xor 53 2200 2202
+2204 const 57 00000
+2205 slice 576 2203 26 0
+2206 concat 53 2205 2204
+2207 xor 53 2203 2206
+2208 ite 53 2037 2207 54
+2209 ite 53 48 54 2208
+2210 ite 53 50 54 2209
+2211 ite 53 2041 54 2210
+2212 ite 53 2044 2211 54
+2213 ite 53 20 2212 2196
+2214 next 53 54 2213
+2215 uext 55 30 11
+2216 add 55 56 2215
+2217 ite 55 2037 2216 56
+2218 ite 55 48 56 2217
+2219 ite 55 50 56 2218
+2220 const 55 000000000001
+2221 ite 55 2041 2220 2219
+2222 ite 55 2044 2221 56
+2223 ite 55 20 2222 56
+2224 next 55 56 2223
+2225 const 57 00001
+2226 redor 1 56
+2227 not 1 2226
+2228 ite 57 2227 2225 58
+2229 ite 57 2037 2228 58
+2230 ite 57 48 58 2229
+2231 ite 57 50 58 2230
+2232 slice 17 58 3 0
+2233 concat 57 2232 9
+2234 ite 57 2041 2233 2231
+2235 ite 57 2044 2234 58
+2236 ite 57 20 2235 2225
+2237 next 57 58 2236
+2238 ite 1 1073 1072 63
+2239 ite 1 20 2238 9
+2240 next 1 63 2239
+2241 next 1 66 3
+2242 ite 1 1073 1071 69
+2243 ite 1 20 2242 69
+2244 next 1 69 2243
+2245 ite 53 84 586 71
+2246 const 53 11111111111111111111111111111111
+2247 ite 53 590 2246 2245
+2248 next 53 71 2247
+2249 not 1 75
+2250 or 1 2249 77
+2251 ite 1 2250 30 73
+2252 const 17 1011
+2253 eq 1 1347 2252
+2254 eq 1 1347 2098
+2255 eq 1 1347 2100
+2256 eq 1 1347 2102
+2257 concat 258 2254 2253
+2258 concat 260 2255 2257
+2259 concat 17 2256 2258
+2260 redor 1 2259
+2261 ite 1 2260 2251 73
+2262 uext 25 9 8
+2263 eq 1 2262 1362
+2264 neq 1 29 1337
+2265 uext 266 2102 3
+2266 ult 1 1348 2265
+2267 and 1 2264 2266
+2268 ite 1 2267 73 2263
+2269 ite 1 2250 2268 73
+2270 const 260 101
+2271 uext 17 2270 1
+2272 eq 1 1347 2271
+2273 ite 1 2272 2269 2261
+2274 ite 1 2250 9 73
+2275 redor 1 1347
+2276 not 1 2275
+2277 ite 1 2276 2274 2273
+2278 not 1 1076
+2279 redor 1 1075
+2280 not 1 2279
+2281 and 1 2278 2280
+2282 ite 1 2281 2277 73
+2283 ite 1 80 2282 73
+2284 ite 1 1349 73 2283
+2285 ite 1 20 2284 73
+2286 next 1 73 2285
+2287 ite 1 77 9 75
+2288 ite 1 2250 9 75
+2289 ite 1 2250 30 75
+2290 const 17 1101
+2291 eq 1 1347 2290
+2292 const 17 1100
+2293 eq 1 1347 2292
+2294 const 260 111
+2295 uext 17 2294 1
+2296 eq 1 1347 2295
+2297 uext 17 2104 1
+2298 eq 1 1347 2297
+2299 uext 17 2107 1
+2300 eq 1 1347 2299
+2301 uext 17 2110 2
+2302 eq 1 1347 2301
+2303 uext 17 2113 2
+2304 eq 1 1347 2303
+2305 uext 17 30 3
+2306 eq 1 1347 2305
+2307 concat 258 2293 2291
+2308 concat 260 2253 2307
+2309 concat 17 2254 2308
+2310 concat 57 2255 2309
+2311 concat 264 2256 2310
+2312 concat 266 2296 2311
+2313 concat 28 2298 2312
+2314 concat 25 2272 2313
+2315 concat 87 2300 2314
+2316 concat 545 2302 2315
+2317 concat 55 2304 2316
+2318 concat 548 2306 2317
+2319 concat 550 2276 2318
+2320 redor 1 2319
+2321 ite 1 2320 2289 2288
+2322 ite 1 2281 2321 2287
+2323 ite 1 80 2322 9
+2324 const 57 10000
+2325 uext 266 2324 2
+2326 ult 1 1348 2325
+2327 ite 1 2326 30 9
+2328 and 1 2250 2280
+2329 ite 1 2328 2327 75
+2330 ite 1 1349 2329 2323
+2331 ite 1 20 2330 9
+2332 next 1 75 2331
+2333 slice 87 855 14 5
+2334 redor 1 2333
+2335 not 1 2334
+2336 and 1 2335 75
+2337 ite 1 2336 75 9
+2338 ite 1 20 2337 9
+2339 next 1 77 2338
+2340 ite 1 1076 9 80
+2341 ite 1 1077 30 2340
+2342 ite 1 20 2341 9
+2343 next 1 80 2342
+2344 slice 25 88 9 1
+2345 concat 87 66 2344
+2346 uext 17 30 3
+2347 eq 1 594 2346
+2348 ite 87 2347 2345 88
+2349 slice 25 2348 9 1
+2350 concat 87 66 2349
+2351 uext 17 2110 2
+2352 eq 1 594 2351
+2353 ite 87 2352 2350 2348
+2354 slice 25 2353 9 1
+2355 concat 87 66 2354
+2356 uext 17 2270 1
+2357 eq 1 594 2356
+2358 ite 87 2357 2355 2353
+2359 slice 25 2358 9 1
+2360 concat 87 66 2359
+2361 uext 17 2294 1
+2362 eq 1 594 2361
+2363 ite 87 2362 2360 2358
+2364 eq 1 66 847
+2365 ite 87 2364 2363 2345
+2366 uext 87 743 3
+2367 eq 1 2365 2366
+2368 uext 17 30 3
+2369 add 17 596 2368
+2370 ite 17 2347 2369 596
+2371 uext 17 30 3
+2372 add 17 2370 2371
+2373 ite 17 2352 2372 2370
+2374 uext 17 30 3
+2375 add 17 2373 2374
+2376 ite 17 2357 2375 2373
+2377 uext 17 30 3
+2378 add 17 2376 2377
+2379 ite 17 2362 2378 2376
+2380 ite 17 2364 2379 2369
+2381 eq 1 2380 2098
+2382 or 1 2367 2381
+2383 ite 1 2382 2136 9
+2384 next 1 82 2383
+2385 ite 25 2250 1011 86
+2386 ite 25 2291 2385 86
+2387 slice 28 71 31 24
+2388 concat 25 9 2387
+2389 ite 25 2250 2388 86
+2390 ite 25 2293 2389 2386
+2391 slice 28 71 23 16
+2392 concat 25 9 2391
+2393 ite 25 2250 2392 86
+2394 ite 25 2253 2393 2390
+2395 slice 28 71 15 8
+2396 concat 25 9 2395
+2397 ite 25 2250 2396 86
+2398 ite 25 2254 2397 2394
+2399 slice 28 71 7 0
+2400 concat 25 9 2399
+2401 ite 25 2250 2400 86
+2402 ite 25 2255 2401 2398
+2403 const 25 110111100
+2404 ite 25 2250 2403 86
+2405 ite 25 2256 2404 2402
+2406 ite 25 2250 1009 86
+2407 ite 25 2296 2406 2405
+2408 const 25 110011100
+2409 ite 25 2250 2408 86
+2410 ite 25 2298 2409 2407
+2411 const 264 111100
+2412 const 264 011100
+2413 uext 25 9 8
+2414 neq 1 2413 1362
+2415 ite 264 2414 2412 2411
+2416 concat 25 2104 2415
+2417 slice 1 1337 0 0
+2418 ite 25 2417 1190 1079
+2419 ite 25 2417 1268 1257
+2420 slice 1 1337 1 1
+2421 ite 25 2420 2419 2418
+2422 ite 25 2417 1290 1279
+2423 ite 25 2417 1312 1301
+2424 ite 25 2420 2423 2422
+2425 slice 1 1337 2 2
+2426 ite 25 2425 2424 2421
+2427 ite 25 2417 1334 1323
+2428 ite 25 2417 1101 1090
+2429 ite 25 2420 2428 2427
+2430 ite 25 2417 1123 1112
+2431 ite 25 2417 1145 1134
+2432 ite 25 2420 2431 2430
+2433 ite 25 2425 2432 2429
+2434 slice 1 1337 3 3
+2435 ite 25 2434 2433 2426
+2436 ite 25 2417 1167 1156
+2437 ite 25 2417 1189 1178
+2438 ite 25 2420 2437 2436
+2439 ite 25 2417 1212 1201
+2440 ite 25 2417 1234 1223
+2441 ite 25 2420 2440 2439
+2442 ite 25 2425 2441 2438
+2443 ite 25 2417 1252 1245
+2444 ite 25 2417 1254 1253
+2445 ite 25 2420 2444 2443
+2446 ite 25 2417 1256 1255
+2447 ite 25 2417 1259 1258
+2448 ite 25 2420 2447 2446
+2449 ite 25 2425 2448 2445
+2450 ite 25 2434 2449 2442
+2451 slice 1 1337 4 4
+2452 ite 25 2451 2450 2435
+2453 ite 25 2417 1261 1260
+2454 ite 25 2417 1263 1262
+2455 ite 25 2420 2454 2453
+2456 ite 25 2417 1265 1264
+2457 ite 25 2417 1267 1266
+2458 ite 25 2420 2457 2456
+2459 ite 25 2425 2458 2455
+2460 ite 25 2417 1270 1269
+2461 ite 25 2417 1272 1271
+2462 ite 25 2420 2461 2460
+2463 ite 25 2417 1274 1273
+2464 ite 25 2417 1276 1275
+2465 ite 25 2420 2464 2463
+2466 ite 25 2425 2465 2462
+2467 ite 25 2434 2466 2459
+2468 ite 25 2417 1278 1277
+2469 ite 25 2417 1281 1280
+2470 ite 25 2420 2469 2468
+2471 ite 25 2417 1283 1282
+2472 ite 25 2417 1285 1284
+2473 ite 25 2420 2472 2471
+2474 ite 25 2425 2473 2470
+2475 ite 25 2417 1287 1286
+2476 ite 25 2417 1289 1288
+2477 ite 25 2420 2476 2475
+2478 ite 25 2417 1292 1291
+2479 ite 25 2417 1294 1293
+2480 ite 25 2420 2479 2478
+2481 ite 25 2425 2480 2477
+2482 ite 25 2434 2481 2474
+2483 ite 25 2451 2482 2467
+2484 slice 1 1337 5 5
+2485 ite 25 2484 2483 2452
+2486 ite 25 2417 1296 1295
+2487 ite 25 2417 1298 1297
+2488 ite 25 2420 2487 2486
+2489 ite 25 2417 1300 1299
+2490 ite 25 2417 1303 1302
+2491 ite 25 2420 2490 2489
+2492 ite 25 2425 2491 2488
+2493 ite 25 2417 1305 1304
+2494 ite 25 2417 1307 1306
+2495 ite 25 2420 2494 2493
+2496 ite 25 2417 1309 1308
+2497 ite 25 2417 1311 1310
+2498 ite 25 2420 2497 2496
+2499 ite 25 2425 2498 2495
+2500 ite 25 2434 2499 2492
+2501 ite 25 2417 1314 1313
+2502 ite 25 2417 1316 1315
+2503 ite 25 2420 2502 2501
+2504 ite 25 2417 1318 1317
+2505 ite 25 2417 1320 1319
+2506 ite 25 2420 2505 2504
+2507 ite 25 2425 2506 2503
+2508 ite 25 2417 1322 1321
+2509 ite 25 2417 1325 1324
+2510 ite 25 2420 2509 2508
+2511 ite 25 2417 1327 1326
+2512 ite 25 2417 1329 1328
+2513 ite 25 2420 2512 2511
+2514 ite 25 2425 2513 2510
+2515 ite 25 2434 2514 2507
+2516 ite 25 2451 2515 2500
+2517 ite 25 2417 1331 1330
+2518 ite 25 2417 1333 1332
+2519 ite 25 2420 2518 2517
+2520 ite 25 2417 1081 1080
+2521 ite 25 2417 1083 1082
+2522 ite 25 2420 2521 2520
+2523 ite 25 2425 2522 2519
+2524 ite 25 2417 1085 1084
+2525 ite 25 2417 1087 1086
+2526 ite 25 2420 2525 2524
+2527 ite 25 2417 1089 1088
+2528 ite 25 2417 1092 1091
+2529 ite 25 2420 2528 2527
+2530 ite 25 2425 2529 2526
+2531 ite 25 2434 2530 2523
+2532 ite 25 2417 1094 1093
+2533 ite 25 2417 1096 1095
+2534 ite 25 2420 2533 2532
+2535 ite 25 2417 1098 1097
+2536 ite 25 2417 1100 1099
+2537 ite 25 2420 2536 2535
+2538 ite 25 2425 2537 2534
+2539 ite 25 2417 1103 1102
+2540 ite 25 2417 1105 1104
+2541 ite 25 2420 2540 2539
+2542 ite 25 2417 1107 1106
+2543 ite 25 2417 1109 1108
+2544 ite 25 2420 2543 2542
+2545 ite 25 2425 2544 2541
+2546 ite 25 2434 2545 2538
+2547 ite 25 2451 2546 2531
+2548 ite 25 2484 2547 2516
+2549 slice 1 1337 6 6
+2550 ite 25 2549 2548 2485
+2551 ite 25 2417 1111 1110
+2552 ite 25 2417 1114 1113
+2553 ite 25 2420 2552 2551
+2554 ite 25 2417 1116 1115
+2555 ite 25 2417 1118 1117
+2556 ite 25 2420 2555 2554
+2557 ite 25 2425 2556 2553
+2558 ite 25 2417 1120 1119
+2559 ite 25 2417 1122 1121
+2560 ite 25 2420 2559 2558
+2561 ite 25 2417 1125 1124
+2562 ite 25 2417 1127 1126
+2563 ite 25 2420 2562 2561
+2564 ite 25 2425 2563 2560
+2565 ite 25 2434 2564 2557
+2566 ite 25 2417 1129 1128
+2567 ite 25 2417 1131 1130
+2568 ite 25 2420 2567 2566
+2569 ite 25 2417 1133 1132
+2570 ite 25 2417 1136 1135
+2571 ite 25 2420 2570 2569
+2572 ite 25 2425 2571 2568
+2573 ite 25 2417 1138 1137
+2574 ite 25 2417 1140 1139
+2575 ite 25 2420 2574 2573
+2576 ite 25 2417 1142 1141
+2577 ite 25 2417 1144 1143
+2578 ite 25 2420 2577 2576
+2579 ite 25 2425 2578 2575
+2580 ite 25 2434 2579 2572
+2581 ite 25 2451 2580 2565
+2582 ite 25 2417 1147 1146
+2583 ite 25 2417 1149 1148
+2584 ite 25 2420 2583 2582
+2585 ite 25 2417 1151 1150
+2586 ite 25 2417 1153 1152
+2587 ite 25 2420 2586 2585
+2588 ite 25 2425 2587 2584
+2589 ite 25 2417 1155 1154
+2590 ite 25 2417 1158 1157
+2591 ite 25 2420 2590 2589
+2592 ite 25 2417 1160 1159
+2593 ite 25 2417 1162 1161
+2594 ite 25 2420 2593 2592
+2595 ite 25 2425 2594 2591
+2596 ite 25 2434 2595 2588
+2597 ite 25 2417 1164 1163
+2598 ite 25 2417 1166 1165
+2599 ite 25 2420 2598 2597
+2600 ite 25 2417 1169 1168
+2601 ite 25 2417 1171 1170
+2602 ite 25 2420 2601 2600
+2603 ite 25 2425 2602 2599
+2604 ite 25 2417 1173 1172
+2605 ite 25 2417 1175 1174
+2606 ite 25 2420 2605 2604
+2607 ite 25 2417 1177 1176
+2608 ite 25 2417 1180 1179
+2609 ite 25 2420 2608 2607
+2610 ite 25 2425 2609 2606
+2611 ite 25 2434 2610 2603
+2612 ite 25 2451 2611 2596
+2613 ite 25 2484 2612 2581
+2614 ite 25 2417 1182 1181
+2615 ite 25 2417 1184 1183
+2616 ite 25 2420 2615 2614
+2617 ite 25 2417 1186 1185
+2618 ite 25 2417 1188 1187
+2619 ite 25 2420 2618 2617
+2620 ite 25 2425 2619 2616
+2621 ite 25 2417 1192 1191
+2622 ite 25 2417 1194 1193
+2623 ite 25 2420 2622 2621
+2624 ite 25 2417 1196 1195
+2625 ite 25 2417 1198 1197
+2626 ite 25 2420 2625 2624
+2627 ite 25 2425 2626 2623
+2628 ite 25 2434 2627 2620
+2629 ite 25 2417 1200 1199
+2630 ite 25 2417 1203 1202
+2631 ite 25 2420 2630 2629
+2632 ite 25 2417 1205 1204
+2633 ite 25 2417 1207 1206
+2634 ite 25 2420 2633 2632
+2635 ite 25 2425 2634 2631
+2636 ite 25 2417 1209 1208
+2637 ite 25 2417 1211 1210
+2638 ite 25 2420 2637 2636
+2639 ite 25 2417 1214 1213
+2640 ite 25 2417 1216 1215
+2641 ite 25 2420 2640 2639
+2642 ite 25 2425 2641 2638
+2643 ite 25 2434 2642 2635
+2644 ite 25 2451 2643 2628
+2645 ite 25 2417 1218 1217
+2646 ite 25 2417 1220 1219
+2647 ite 25 2420 2646 2645
+2648 ite 25 2417 1222 1221
+2649 ite 25 2417 1225 1224
+2650 ite 25 2420 2649 2648
+2651 ite 25 2425 2650 2647
+2652 ite 25 2417 1227 1226
+2653 ite 25 2417 1229 1228
+2654 ite 25 2420 2653 2652
+2655 ite 25 2417 1231 1230
+2656 ite 25 2417 1233 1232
+2657 ite 25 2420 2656 2655
+2658 ite 25 2425 2657 2654
+2659 ite 25 2434 2658 2651
+2660 ite 25 2417 1236 1235
+2661 ite 25 2417 1238 1237
+2662 ite 25 2420 2661 2660
+2663 ite 25 2417 1240 1239
+2664 ite 25 2417 1242 1241
+2665 ite 25 2420 2664 2663
+2666 ite 25 2425 2665 2662
+2667 ite 25 2417 1244 1243
+2668 ite 25 2417 1247 1246
+2669 ite 25 2420 2668 2667
+2670 ite 25 2417 1249 1248
+2671 ite 25 2417 1251 1250
+2672 ite 25 2420 2671 2670
+2673 ite 25 2425 2672 2669
+2674 ite 25 2434 2673 2666
+2675 ite 25 2451 2674 2659
+2676 ite 25 2484 2675 2644
+2677 ite 25 2549 2676 2613
+2678 slice 1 1337 7 7
+2679 ite 25 2678 2677 2550
+2680 ite 25 2267 2679 2416
+2681 ite 25 2250 2680 86
+2682 ite 25 2272 2681 2410
+2683 concat 25 9 33
+2684 ite 25 2250 2683 86
+2685 ite 25 2300 2684 2682
+2686 concat 25 9 42
+2687 ite 25 2250 2686 86
+2688 ite 25 2302 2687 2685
+2689 const 25 001110100
+2690 ite 25 2250 2689 86
+2691 ite 25 2304 2690 2688
+2692 ite 25 2250 588 86
+2693 ite 25 2306 2692 2691
+2694 const 25 010110101
+2695 ite 25 2250 2694 86
+2696 ite 25 2276 2695 2693
+2697 ite 25 2281 2696 86
+2698 ite 25 80 2697 86
+2699 const 258 00
+2700 concat 25 2699 1348
+2701 uext 266 2052 3
+2702 eq 1 1348 2701
+2703 ite 25 2702 1011 2700
+2704 const 25 111111110
+2705 uext 266 2270 4
+2706 eq 1 1348 2705
+2707 uext 266 2107 4
+2708 eq 1 1348 2707
+2709 uext 266 2110 5
+2710 eq 1 1348 2709
+2711 uext 266 2113 5
+2712 eq 1 1348 2711
+2713 concat 258 2708 2706
+2714 concat 260 2710 2713
+2715 concat 17 2712 2714
+2716 redor 1 2715
+2717 ite 25 2716 2704 2703
+2718 uext 266 30 6
+2719 eq 1 1348 2718
+2720 ite 25 2719 588 2717
+2721 redor 1 1348
+2722 not 1 2721
+2723 ite 25 2722 2694 2720
+2724 ite 25 2326 2723 86
+2725 ite 25 2328 2724 86
+2726 ite 25 1349 2725 2698
+2727 ite 25 20 2726 86
+2728 next 25 86 2727
+2729 next 87 88 2365
+2730 uext 17 30 3
+2731 add 17 594 2730
+2732 ite 17 2364 2731 593
+2733 next 17 594 2732
+2734 ite 17 2382 593 2380
+2735 next 17 596 2734
+2736 ite 1 82 803 742
+2737 next 1 742 2736
+2738 uext 17 30 3
+2739 add 17 845 2738
+2740 uext 25 845 5
+2741 eq 1 269 2740
+2742 ite 17 2741 2739 593
+2743 uext 17 2104 1
+2744 ulte 1 2743 845
+2745 ite 17 2744 2742 593
+2746 const 25 111111101
+2747 eq 1 269 2746
+2748 ite 17 2747 2739 593
+2749 uext 17 2113 2
+2750 ulte 1 2749 845
+2751 uext 17 2104 1
+2752 ult 1 845 2751
+2753 and 1 2750 2752
+2754 ite 17 2753 2748 2745
+2755 const 17 0010
+2756 ite 17 2130 2755 2754
+2757 ite 17 842 593 2756
+2758 ite 17 82 2757 845
+2759 ite 17 63 593 2758
+2760 eq 1 845 2052
+2761 ite 17 2760 593 2759
+2762 next 17 845 2761
+2763 ite 1 2760 30 9
+2764 next 1 846 2763
+2765 next 1 847 66
+2766 slice 87 854 14 5
+2767 ite 87 2336 1013 2766
+2768 slice 57 854 4 0
+2769 concat 552 2767 2768
+2770 slice 17 854 4 1
+2771 concat 550 2767 2770
+2772 concat 552 9 2771
+2773 ite 552 1073 2772 2769
+2774 ite 552 20 2773 854
+2775 next 552 854 2774
+2776 const 552 000000000000000
+2777 concat 258 75 75
+2778 concat 260 75 2777
+2779 concat 17 75 2778
+2780 concat 57 75 2779
+2781 concat 264 75 2780
+2782 concat 266 75 2781
+2783 concat 28 75 2782
+2784 concat 25 75 2783
+2785 concat 87 75 2784
+2786 ite 87 2336 2785 2333
+2787 slice 57 855 4 0
+2788 concat 552 2786 2787
+2789 slice 17 855 4 1
+2790 concat 550 2786 2789
+2791 concat 552 9 2790
+2792 ite 552 1073 2791 2788
+2793 ite 552 20 2792 2776
+2794 next 552 855 2793
+2795 eq 1 1065 2107
+2796 uext 260 2110 1
+2797 eq 1 1065 2796
+2798 uext 260 2113 1
+2799 eq 1 1065 2798
+2800 uext 260 30 2
+2801 eq 1 1065 2800
+2802 concat 258 2797 2795
+2803 concat 260 2799 2802
+2804 concat 17 2801 2803
+2805 redor 1 2804
+2806 ite 260 2805 858 857
+2807 not 1 1072
+2808 neq 1 1062 1071
+2809 or 1 2807 2808
+2810 eq 1 1065 2270
+2811 or 1 2809 2810
+2812 ite 260 2811 857 2806
+2813 ite 260 1073 2812 858
+2814 uext 260 30 2
+2815 add 260 2813 2814
+2816 ite 260 20 2815 857
+2817 next 260 858 2816
+2818 ite 1 2336 1018 901
+2819 ite 1 20 2818 9
+2820 next 1 901 2819
+2821 slice 1 1013 9 9
+2822 next 1 1007 2821
+2823 ite 1 1073 1071 1062
+2824 ite 1 20 2823 9
+2825 next 1 1062 2824
+2826 ite 260 2795 2270 1064
+2827 ite 260 2797 2107 2826
+2828 const 260 011
+2829 ite 260 2799 2828 2827
+2830 const 260 010
+2831 ite 260 2801 2830 2829
+2832 ite 260 2811 1064 2831
+2833 ite 260 1073 2832 1065
+2834 ite 260 20 2833 1064
+2835 next 260 1065 2834
+2836 slice 1 2773 0 0
+2837 ite 1 20 2836 1071
+2838 next 1 1071 2837
+2839 slice 1 2792 0 0
+2840 ite 1 20 2839 9
+2841 next 1 1072 2840
+2842 eq 1 2833 2815
+2843 ite 1 2842 30 9
+2844 ite 1 20 2843 9
+2845 next 1 1073 2844
+2846 uext 260 30 2
+2847 sub 260 1074 2846
+2848 redor 1 1074
+2849 ite 260 2848 2847 1074
+2850 ite 260 1076 2294 2849
+2851 ite 260 1077 2849 2850
+2852 ite 260 20 2851 2294
+2853 next 260 1074 2852
+2854 const 57 11111
+2855 uext 57 30 4
+2856 sub 57 1075 2855
+2857 redor 1 1075
+2858 ite 57 2857 2856 1075
+2859 ite 57 1077 2854 2858
+2860 ite 57 20 2859 2854
+2861 next 57 1075 2860
+2862 ite 1 63 9 30
+2863 ite 1 2250 2862 9
+2864 ite 1 2320 9 2863
+2865 ite 1 2281 2864 9
+2866 ite 1 80 2865 9
+2867 ite 1 2326 9 30
+2868 ite 1 2328 2867 9
+2869 ite 1 1349 2868 2866
+2870 ite 1 20 2869 9
+2871 next 1 1076 2870
+2872 ite 1 2128 846 30
+2873 ite 1 2130 846 2872
+2874 ite 1 842 846 2873
+2875 ite 1 2137 2874 846
+2876 ite 1 80 846 2875
+2877 ite 1 20 2876 846
+2878 next 1 1077 2877
+2879 eq 1 269 2403
+2880 ite 53 2879 71 1078
+2881 ite 53 2106 2880 1078
+2882 eq 1 269 2408
+2883 ite 53 2882 1078 2880
+2884 ite 53 2109 2883 2881
+2885 ite 53 2130 1078 2884
+2886 ite 53 842 1078 2885
+2887 ite 53 2137 2886 1078
+2888 ite 53 80 1078 2887
+2889 ite 53 20 2888 1078
+2890 next 53 1078 2889
+2891 slice 1 29 0 0
+2892 not 1 2891
+2893 slice 1 29 1 1
+2894 not 1 2893
+2895 and 1 2892 2894
+2896 slice 1 29 2 2
+2897 not 1 2896
+2898 slice 1 29 3 3
+2899 not 1 2898
+2900 and 1 2897 2899
+2901 and 1 2895 2900
+2902 slice 1 29 4 4
+2903 not 1 2902
+2904 slice 1 29 5 5
+2905 not 1 2904
+2906 and 1 2903 2905
+2907 slice 1 29 6 6
+2908 not 1 2907
+2909 slice 1 29 7 7
+2910 not 1 2909
+2911 and 1 2908 2910
+2912 and 1 2906 2911
+2913 and 1 2901 2912
+2914 ite 1 2090 30 9
+2915 ite 1 20 2914 9
+2916 and 1 2913 2915
+2917 ite 25 2916 26 1079
+2918 next 25 1079 2917
+2919 and 1 2896 2899
+2920 and 1 2895 2919
+2921 and 1 2903 2904
+2922 and 1 2907 2910
+2923 and 1 2921 2922
+2924 and 1 2920 2923
+2925 and 1 2924 2915
+2926 ite 25 2925 26 1080
+2927 next 25 1080 2926
+2928 and 1 2891 2894
+2929 and 1 2928 2919
+2930 and 1 2929 2923
+2931 and 1 2930 2915
+2932 ite 25 2931 26 1081
+2933 next 25 1081 2932
+2934 and 1 2892 2893
+2935 and 1 2934 2919
+2936 and 1 2935 2923
+2937 and 1 2936 2915
+2938 ite 25 2937 26 1082
+2939 next 25 1082 2938
+2940 and 1 2891 2893
+2941 and 1 2940 2919
+2942 and 1 2941 2923
+2943 and 1 2942 2915
+2944 ite 25 2943 26 1083
+2945 next 25 1083 2944
+2946 and 1 2897 2898
+2947 and 1 2895 2946
+2948 and 1 2947 2923
+2949 and 1 2948 2915
+2950 ite 25 2949 26 1084
+2951 next 25 1084 2950
+2952 and 1 2928 2946
+2953 and 1 2952 2923
+2954 and 1 2953 2915
+2955 ite 25 2954 26 1085
+2956 next 25 1085 2955
+2957 and 1 2934 2946
+2958 and 1 2957 2923
+2959 and 1 2958 2915
+2960 ite 25 2959 26 1086
+2961 next 25 1086 2960
+2962 and 1 2940 2946
+2963 and 1 2962 2923
+2964 and 1 2963 2915
+2965 ite 25 2964 26 1087
+2966 next 25 1087 2965
+2967 and 1 2896 2898
+2968 and 1 2895 2967
+2969 and 1 2968 2923
+2970 and 1 2969 2915
+2971 ite 25 2970 26 1088
+2972 next 25 1088 2971
+2973 and 1 2928 2967
+2974 and 1 2973 2923
+2975 and 1 2974 2915
+2976 ite 25 2975 26 1089
+2977 next 25 1089 2976
+2978 and 1 2957 2912
+2979 and 1 2978 2915
+2980 ite 25 2979 26 1090
+2981 next 25 1090 2980
+2982 and 1 2934 2967
+2983 and 1 2982 2923
+2984 and 1 2983 2915
+2985 ite 25 2984 26 1091
+2986 next 25 1091 2985
+2987 and 1 2940 2967
+2988 and 1 2987 2923
+2989 and 1 2988 2915
+2990 ite 25 2989 26 1092
+2991 next 25 1092 2990
+2992 and 1 2902 2904
+2993 and 1 2992 2922
+2994 and 1 2901 2993
+2995 and 1 2994 2915
+2996 ite 25 2995 26 1093
+2997 next 25 1093 2996
+2998 and 1 2928 2900
+2999 and 1 2998 2993
+3000 and 1 2999 2915
+3001 ite 25 3000 26 1094
+3002 next 25 1094 3001
+3003 and 1 2934 2900
+3004 and 1 3003 2993
+3005 and 1 3004 2915
+3006 ite 25 3005 26 1095
+3007 next 25 1095 3006
+3008 and 1 2940 2900
+3009 and 1 3008 2993
+3010 and 1 3009 2915
+3011 ite 25 3010 26 1096
+3012 next 25 1096 3011
+3013 and 1 2920 2993
+3014 and 1 3013 2915
+3015 ite 25 3014 26 1097
+3016 next 25 1097 3015
+3017 and 1 2929 2993
+3018 and 1 3017 2915
+3019 ite 25 3018 26 1098
+3020 next 25 1098 3019
+3021 and 1 2935 2993
+3022 and 1 3021 2915
+3023 ite 25 3022 26 1099
+3024 next 25 1099 3023
+3025 and 1 2941 2993
+3026 and 1 3025 2915
+3027 ite 25 3026 26 1100
+3028 next 25 1100 3027
+3029 and 1 2962 2912
+3030 and 1 3029 2915
+3031 ite 25 3030 26 1101
+3032 next 25 1101 3031
+3033 and 1 2947 2993
+3034 and 1 3033 2915
+3035 ite 25 3034 26 1102
+3036 next 25 1102 3035
+3037 and 1 2952 2993
+3038 and 1 3037 2915
+3039 ite 25 3038 26 1103
+3040 next 25 1103 3039
+3041 and 1 2957 2993
+3042 and 1 3041 2915
+3043 ite 25 3042 26 1104
+3044 next 25 1104 3043
+3045 and 1 2962 2993
+3046 and 1 3045 2915
+3047 ite 25 3046 26 1105
+3048 next 25 1105 3047
+3049 and 1 2968 2993
+3050 and 1 3049 2915
+3051 ite 25 3050 26 1106
+3052 next 25 1106 3051
+3053 and 1 2973 2993
+3054 and 1 3053 2915
+3055 ite 25 3054 26 1107
+3056 next 25 1107 3055
+3057 and 1 2982 2993
+3058 and 1 3057 2915
+3059 ite 25 3058 26 1108
+3060 next 25 1108 3059
+3061 and 1 2987 2993
+3062 and 1 3061 2915
+3063 ite 25 3062 26 1109
+3064 next 25 1109 3063
+3065 and 1 2908 2909
+3066 and 1 2906 3065
+3067 and 1 2901 3066
+3068 and 1 3067 2915
+3069 ite 25 3068 26 1110
+3070 next 25 1110 3069
+3071 and 1 2998 3066
+3072 and 1 3071 2915
+3073 ite 25 3072 26 1111
+3074 next 25 1111 3073
+3075 and 1 2968 2912
+3076 and 1 3075 2915
+3077 ite 25 3076 26 1112
+3078 next 25 1112 3077
+3079 and 1 3003 3066
+3080 and 1 3079 2915
+3081 ite 25 3080 26 1113
+3082 next 25 1113 3081
+3083 and 1 3008 3066
+3084 and 1 3083 2915
+3085 ite 25 3084 26 1114
+3086 next 25 1114 3085
+3087 and 1 2920 3066
+3088 and 1 3087 2915
+3089 ite 25 3088 26 1115
+3090 next 25 1115 3089
+3091 and 1 2929 3066
+3092 and 1 3091 2915
+3093 ite 25 3092 26 1116
+3094 next 25 1116 3093
+3095 and 1 2935 3066
+3096 and 1 3095 2915
+3097 ite 25 3096 26 1117
+3098 next 25 1117 3097
+3099 and 1 2941 3066
+3100 and 1 3099 2915
+3101 ite 25 3100 26 1118
+3102 next 25 1118 3101
+3103 and 1 2947 3066
+3104 and 1 3103 2915
+3105 ite 25 3104 26 1119
+3106 next 25 1119 3105
+3107 and 1 2952 3066
+3108 and 1 3107 2915
+3109 ite 25 3108 26 1120
+3110 next 25 1120 3109
+3111 and 1 2957 3066
+3112 and 1 3111 2915
+3113 ite 25 3112 26 1121
+3114 next 25 1121 3113
+3115 and 1 2962 3066
+3116 and 1 3115 2915
+3117 ite 25 3116 26 1122
+3118 next 25 1122 3117
+3119 and 1 2973 2912
+3120 and 1 3119 2915
+3121 ite 25 3120 26 1123
+3122 next 25 1123 3121
+3123 and 1 2968 3066
+3124 and 1 3123 2915
+3125 ite 25 3124 26 1124
+3126 next 25 1124 3125
+3127 and 1 2973 3066
+3128 and 1 3127 2915
+3129 ite 25 3128 26 1125
+3130 next 25 1125 3129
+3131 and 1 2982 3066
+3132 and 1 3131 2915
+3133 ite 25 3132 26 1126
+3134 next 25 1126 3133
+3135 and 1 2987 3066
+3136 and 1 3135 2915
+3137 ite 25 3136 26 1127
+3138 next 25 1127 3137
+3139 and 1 2902 2905
+3140 and 1 3139 3065
+3141 and 1 2901 3140
+3142 and 1 3141 2915
+3143 ite 25 3142 26 1128
+3144 next 25 1128 3143
+3145 and 1 2998 3140
+3146 and 1 3145 2915
+3147 ite 25 3146 26 1129
+3148 next 25 1129 3147
+3149 and 1 3003 3140
+3150 and 1 3149 2915
+3151 ite 25 3150 26 1130
+3152 next 25 1130 3151
+3153 and 1 3008 3140
+3154 and 1 3153 2915
+3155 ite 25 3154 26 1131
+3156 next 25 1131 3155
+3157 and 1 2920 3140
+3158 and 1 3157 2915
+3159 ite 25 3158 26 1132
+3160 next 25 1132 3159
+3161 and 1 2929 3140
+3162 and 1 3161 2915
+3163 ite 25 3162 26 1133
+3164 next 25 1133 3163
+3165 and 1 2982 2912
+3166 and 1 3165 2915
+3167 ite 25 3166 26 1134
+3168 next 25 1134 3167
+3169 and 1 2935 3140
+3170 and 1 3169 2915
+3171 ite 25 3170 26 1135
+3172 next 25 1135 3171
+3173 and 1 2941 3140
+3174 and 1 3173 2915
+3175 ite 25 3174 26 1136
+3176 next 25 1136 3175
+3177 and 1 2947 3140
+3178 and 1 3177 2915
+3179 ite 25 3178 26 1137
+3180 next 25 1137 3179
+3181 and 1 2952 3140
+3182 and 1 3181 2915
+3183 ite 25 3182 26 1138
+3184 next 25 1138 3183
+3185 and 1 2957 3140
+3186 and 1 3185 2915
+3187 ite 25 3186 26 1139
+3188 next 25 1139 3187
+3189 and 1 2962 3140
+3190 and 1 3189 2915
+3191 ite 25 3190 26 1140
+3192 next 25 1140 3191
+3193 and 1 2968 3140
+3194 and 1 3193 2915
+3195 ite 25 3194 26 1141
+3196 next 25 1141 3195
+3197 and 1 2973 3140
+3198 and 1 3197 2915
+3199 ite 25 3198 26 1142
+3200 next 25 1142 3199
+3201 and 1 2982 3140
+3202 and 1 3201 2915
+3203 ite 25 3202 26 1143
+3204 next 25 1143 3203
+3205 and 1 2987 3140
+3206 and 1 3205 2915
+3207 ite 25 3206 26 1144
+3208 next 25 1144 3207
+3209 and 1 2987 2912
+3210 and 1 3209 2915
+3211 ite 25 3210 26 1145
+3212 next 25 1145 3211
+3213 and 1 2921 3065
+3214 and 1 2901 3213
+3215 and 1 3214 2915
+3216 ite 25 3215 26 1146
+3217 next 25 1146 3216
+3218 and 1 2998 3213
+3219 and 1 3218 2915
+3220 ite 25 3219 26 1147
+3221 next 25 1147 3220
+3222 and 1 3003 3213
+3223 and 1 3222 2915
+3224 ite 25 3223 26 1148
+3225 next 25 1148 3224
+3226 and 1 3008 3213
+3227 and 1 3226 2915
+3228 ite 25 3227 26 1149
+3229 next 25 1149 3228
+3230 and 1 2920 3213
+3231 and 1 3230 2915
+3232 ite 25 3231 26 1150
+3233 next 25 1150 3232
+3234 and 1 2929 3213
+3235 and 1 3234 2915
+3236 ite 25 3235 26 1151
+3237 next 25 1151 3236
+3238 and 1 2935 3213
+3239 and 1 3238 2915
+3240 ite 25 3239 26 1152
+3241 next 25 1152 3240
+3242 and 1 2941 3213
+3243 and 1 3242 2915
+3244 ite 25 3243 26 1153
+3245 next 25 1153 3244
+3246 and 1 2947 3213
+3247 and 1 3246 2915
+3248 ite 25 3247 26 1154
+3249 next 25 1154 3248
+3250 and 1 2952 3213
+3251 and 1 3250 2915
+3252 ite 25 3251 26 1155
+3253 next 25 1155 3252
+3254 and 1 3139 2911
+3255 and 1 2901 3254
+3256 and 1 3255 2915
+3257 ite 25 3256 26 1156
+3258 next 25 1156 3257
+3259 and 1 2957 3213
+3260 and 1 3259 2915
+3261 ite 25 3260 26 1157
+3262 next 25 1157 3261
+3263 and 1 2962 3213
+3264 and 1 3263 2915
+3265 ite 25 3264 26 1158
+3266 next 25 1158 3265
+3267 and 1 2968 3213
+3268 and 1 3267 2915
+3269 ite 25 3268 26 1159
+3270 next 25 1159 3269
+3271 and 1 2973 3213
+3272 and 1 3271 2915
+3273 ite 25 3272 26 1160
+3274 next 25 1160 3273
+3275 and 1 2982 3213
+3276 and 1 3275 2915
+3277 ite 25 3276 26 1161
+3278 next 25 1161 3277
+3279 and 1 2987 3213
+3280 and 1 3279 2915
+3281 ite 25 3280 26 1162
+3282 next 25 1162 3281
+3283 and 1 2992 3065
+3284 and 1 2901 3283
+3285 and 1 3284 2915
+3286 ite 25 3285 26 1163
+3287 next 25 1163 3286
+3288 and 1 2998 3283
+3289 and 1 3288 2915
+3290 ite 25 3289 26 1164
+3291 next 25 1164 3290
+3292 and 1 3003 3283
+3293 and 1 3292 2915
+3294 ite 25 3293 26 1165
+3295 next 25 1165 3294
+3296 and 1 3008 3283
+3297 and 1 3296 2915
+3298 ite 25 3297 26 1166
+3299 next 25 1166 3298
+3300 and 1 2998 3254
+3301 and 1 3300 2915
+3302 ite 25 3301 26 1167
+3303 next 25 1167 3302
+3304 and 1 2920 3283
+3305 and 1 3304 2915
+3306 ite 25 3305 26 1168
+3307 next 25 1168 3306
+3308 and 1 2929 3283
+3309 and 1 3308 2915
+3310 ite 25 3309 26 1169
+3311 next 25 1169 3310
+3312 and 1 2935 3283
+3313 and 1 3312 2915
+3314 ite 25 3313 26 1170
+3315 next 25 1170 3314
+3316 and 1 2941 3283
+3317 and 1 3316 2915
+3318 ite 25 3317 26 1171
+3319 next 25 1171 3318
+3320 and 1 2947 3283
+3321 and 1 3320 2915
+3322 ite 25 3321 26 1172
+3323 next 25 1172 3322
+3324 and 1 2952 3283
+3325 and 1 3324 2915
+3326 ite 25 3325 26 1173
+3327 next 25 1173 3326
+3328 and 1 2957 3283
+3329 and 1 3328 2915
+3330 ite 25 3329 26 1174
+3331 next 25 1174 3330
+3332 and 1 2962 3283
+3333 and 1 3332 2915
+3334 ite 25 3333 26 1175
+3335 next 25 1175 3334
+3336 and 1 2968 3283
+3337 and 1 3336 2915
+3338 ite 25 3337 26 1176
+3339 next 25 1176 3338
+3340 and 1 2973 3283
+3341 and 1 3340 2915
+3342 ite 25 3341 26 1177
+3343 next 25 1177 3342
+3344 and 1 3003 3254
+3345 and 1 3344 2915
+3346 ite 25 3345 26 1178
+3347 next 25 1178 3346
+3348 and 1 2982 3283
+3349 and 1 3348 2915
+3350 ite 25 3349 26 1179
+3351 next 25 1179 3350
+3352 and 1 2987 3283
+3353 and 1 3352 2915
+3354 ite 25 3353 26 1180
+3355 next 25 1180 3354
+3356 and 1 2907 2909
+3357 and 1 2906 3356
+3358 and 1 2901 3357
+3359 and 1 3358 2915
+3360 ite 25 3359 26 1181
+3361 next 25 1181 3360
+3362 and 1 2998 3357
+3363 and 1 3362 2915
+3364 ite 25 3363 26 1182
+3365 next 25 1182 3364
+3366 and 1 3003 3357
+3367 and 1 3366 2915
+3368 ite 25 3367 26 1183
+3369 next 25 1183 3368
+3370 and 1 3008 3357
+3371 and 1 3370 2915
+3372 ite 25 3371 26 1184
+3373 next 25 1184 3372
+3374 and 1 2920 3357
+3375 and 1 3374 2915
+3376 ite 25 3375 26 1185
+3377 next 25 1185 3376
+3378 and 1 2929 3357
+3379 and 1 3378 2915
+3380 ite 25 3379 26 1186
+3381 next 25 1186 3380
+3382 and 1 2935 3357
+3383 and 1 3382 2915
+3384 ite 25 3383 26 1187
+3385 next 25 1187 3384
+3386 and 1 2941 3357
+3387 and 1 3386 2915
+3388 ite 25 3387 26 1188
+3389 next 25 1188 3388
+3390 and 1 3008 3254
+3391 and 1 3390 2915
+3392 ite 25 3391 26 1189
+3393 next 25 1189 3392
+3394 and 1 2998 2912
+3395 and 1 3394 2915
+3396 ite 25 3395 26 1190
+3397 next 25 1190 3396
+3398 and 1 2947 3357
+3399 and 1 3398 2915
+3400 ite 25 3399 26 1191
+3401 next 25 1191 3400
+3402 and 1 2952 3357
+3403 and 1 3402 2915
+3404 ite 25 3403 26 1192
+3405 next 25 1192 3404
+3406 and 1 2957 3357
+3407 and 1 3406 2915
+3408 ite 25 3407 26 1193
+3409 next 25 1193 3408
+3410 and 1 2962 3357
+3411 and 1 3410 2915
+3412 ite 25 3411 26 1194
+3413 next 25 1194 3412
+3414 and 1 2968 3357
+3415 and 1 3414 2915
+3416 ite 25 3415 26 1195
+3417 next 25 1195 3416
+3418 and 1 2973 3357
+3419 and 1 3418 2915
+3420 ite 25 3419 26 1196
+3421 next 25 1196 3420
+3422 and 1 2982 3357
+3423 and 1 3422 2915
+3424 ite 25 3423 26 1197
+3425 next 25 1197 3424
+3426 and 1 2987 3357
+3427 and 1 3426 2915
+3428 ite 25 3427 26 1198
+3429 next 25 1198 3428
+3430 and 1 3139 3356
+3431 and 1 2901 3430
+3432 and 1 3431 2915
+3433 ite 25 3432 26 1199
+3434 next 25 1199 3433
+3435 and 1 2998 3430
+3436 and 1 3435 2915
+3437 ite 25 3436 26 1200
+3438 next 25 1200 3437
+3439 and 1 2920 3254
+3440 and 1 3439 2915
+3441 ite 25 3440 26 1201
+3442 next 25 1201 3441
+3443 and 1 3003 3430
+3444 and 1 3443 2915
+3445 ite 25 3444 26 1202
+3446 next 25 1202 3445
+3447 and 1 3008 3430
+3448 and 1 3447 2915
+3449 ite 25 3448 26 1203
+3450 next 25 1203 3449
+3451 and 1 2920 3430
+3452 and 1 3451 2915
+3453 ite 25 3452 26 1204
+3454 next 25 1204 3453
+3455 and 1 2929 3430
+3456 and 1 3455 2915
+3457 ite 25 3456 26 1205
+3458 next 25 1205 3457
+3459 and 1 2935 3430
+3460 and 1 3459 2915
+3461 ite 25 3460 26 1206
+3462 next 25 1206 3461
+3463 and 1 2941 3430
+3464 and 1 3463 2915
+3465 ite 25 3464 26 1207
+3466 next 25 1207 3465
+3467 and 1 2947 3430
+3468 and 1 3467 2915
+3469 ite 25 3468 26 1208
+3470 next 25 1208 3469
+3471 and 1 2952 3430
+3472 and 1 3471 2915
+3473 ite 25 3472 26 1209
+3474 next 25 1209 3473
+3475 and 1 2957 3430
+3476 and 1 3475 2915
+3477 ite 25 3476 26 1210
+3478 next 25 1210 3477
+3479 and 1 2962 3430
+3480 and 1 3479 2915
+3481 ite 25 3480 26 1211
+3482 next 25 1211 3481
+3483 and 1 2929 3254
+3484 and 1 3483 2915
+3485 ite 25 3484 26 1212
+3486 next 25 1212 3485
+3487 and 1 2968 3430
+3488 and 1 3487 2915
+3489 ite 25 3488 26 1213
+3490 next 25 1213 3489
+3491 and 1 2973 3430
+3492 and 1 3491 2915
+3493 ite 25 3492 26 1214
+3494 next 25 1214 3493
+3495 and 1 2982 3430
+3496 and 1 3495 2915
+3497 ite 25 3496 26 1215
+3498 next 25 1215 3497
+3499 and 1 2987 3430
+3500 and 1 3499 2915
+3501 ite 25 3500 26 1216
+3502 next 25 1216 3501
+3503 and 1 2921 3356
+3504 and 1 2901 3503
+3505 and 1 3504 2915
+3506 ite 25 3505 26 1217
+3507 next 25 1217 3506
+3508 and 1 2998 3503
+3509 and 1 3508 2915
+3510 ite 25 3509 26 1218
+3511 next 25 1218 3510
+3512 and 1 3003 3503
+3513 and 1 3512 2915
+3514 ite 25 3513 26 1219
+3515 next 25 1219 3514
+3516 and 1 3008 3503
+3517 and 1 3516 2915
+3518 ite 25 3517 26 1220
+3519 next 25 1220 3518
+3520 and 1 2920 3503
+3521 and 1 3520 2915
+3522 ite 25 3521 26 1221
+3523 next 25 1221 3522
+3524 and 1 2929 3503
+3525 and 1 3524 2915
+3526 ite 25 3525 26 1222
+3527 next 25 1222 3526
+3528 and 1 2935 3254
+3529 and 1 3528 2915
+3530 ite 25 3529 26 1223
+3531 next 25 1223 3530
+3532 and 1 2935 3503
+3533 and 1 3532 2915
+3534 ite 25 3533 26 1224
+3535 next 25 1224 3534
+3536 and 1 2941 3503
+3537 and 1 3536 2915
+3538 ite 25 3537 26 1225
+3539 next 25 1225 3538
+3540 and 1 2947 3503
+3541 and 1 3540 2915
+3542 ite 25 3541 26 1226
+3543 next 25 1226 3542
+3544 and 1 2952 3503
+3545 and 1 3544 2915
+3546 ite 25 3545 26 1227
+3547 next 25 1227 3546
+3548 and 1 2957 3503
+3549 and 1 3548 2915
+3550 ite 25 3549 26 1228
+3551 next 25 1228 3550
+3552 and 1 2962 3503
+3553 and 1 3552 2915
+3554 ite 25 3553 26 1229
+3555 next 25 1229 3554
+3556 and 1 2968 3503
+3557 and 1 3556 2915
+3558 ite 25 3557 26 1230
+3559 next 25 1230 3558
+3560 and 1 2973 3503
+3561 and 1 3560 2915
+3562 ite 25 3561 26 1231
+3563 next 25 1231 3562
+3564 and 1 2982 3503
+3565 and 1 3564 2915
+3566 ite 25 3565 26 1232
+3567 next 25 1232 3566
+3568 and 1 2987 3503
+3569 and 1 3568 2915
+3570 ite 25 3569 26 1233
+3571 next 25 1233 3570
+3572 and 1 2941 3254
+3573 and 1 3572 2915
+3574 ite 25 3573 26 1234
+3575 next 25 1234 3574
+3576 and 1 2992 3356
+3577 and 1 2901 3576
+3578 and 1 3577 2915
+3579 ite 25 3578 26 1235
+3580 next 25 1235 3579
+3581 and 1 2998 3576
+3582 and 1 3581 2915
+3583 ite 25 3582 26 1236
+3584 next 25 1236 3583
+3585 and 1 3003 3576
+3586 and 1 3585 2915
+3587 ite 25 3586 26 1237
+3588 next 25 1237 3587
+3589 and 1 3008 3576
+3590 and 1 3589 2915
+3591 ite 25 3590 26 1238
+3592 next 25 1238 3591
+3593 and 1 2920 3576
+3594 and 1 3593 2915
+3595 ite 25 3594 26 1239
+3596 next 25 1239 3595
+3597 and 1 2929 3576
+3598 and 1 3597 2915
+3599 ite 25 3598 26 1240
+3600 next 25 1240 3599
+3601 and 1 2935 3576
+3602 and 1 3601 2915
+3603 ite 25 3602 26 1241
+3604 next 25 1241 3603
+3605 and 1 2941 3576
+3606 and 1 3605 2915
+3607 ite 25 3606 26 1242
+3608 next 25 1242 3607
+3609 and 1 2947 3576
+3610 and 1 3609 2915
+3611 ite 25 3610 26 1243
+3612 next 25 1243 3611
+3613 and 1 2952 3576
+3614 and 1 3613 2915
+3615 ite 25 3614 26 1244
+3616 next 25 1244 3615
+3617 and 1 2947 3254
+3618 and 1 3617 2915
+3619 ite 25 3618 26 1245
+3620 next 25 1245 3619
+3621 and 1 2957 3576
+3622 and 1 3621 2915
+3623 ite 25 3622 26 1246
+3624 next 25 1246 3623
+3625 and 1 2962 3576
+3626 and 1 3625 2915
+3627 ite 25 3626 26 1247
+3628 next 25 1247 3627
+3629 and 1 2968 3576
+3630 and 1 3629 2915
+3631 ite 25 3630 26 1248
+3632 next 25 1248 3631
+3633 and 1 2973 3576
+3634 and 1 3633 2915
+3635 ite 25 3634 26 1249
+3636 next 25 1249 3635
+3637 and 1 2982 3576
+3638 and 1 3637 2915
+3639 ite 25 3638 26 1250
+3640 next 25 1250 3639
+3641 and 1 2987 3576
+3642 and 1 3641 2915
+3643 ite 25 3642 26 1251
+3644 next 25 1251 3643
+3645 and 1 2952 3254
+3646 and 1 3645 2915
+3647 ite 25 3646 26 1252
+3648 next 25 1252 3647
+3649 and 1 2957 3254
+3650 and 1 3649 2915
+3651 ite 25 3650 26 1253
+3652 next 25 1253 3651
+3653 and 1 2962 3254
+3654 and 1 3653 2915
+3655 ite 25 3654 26 1254
+3656 next 25 1254 3655
+3657 and 1 2968 3254
+3658 and 1 3657 2915
+3659 ite 25 3658 26 1255
+3660 next 25 1255 3659
+3661 and 1 2973 3254
+3662 and 1 3661 2915
+3663 ite 25 3662 26 1256
+3664 next 25 1256 3663
+3665 and 1 3003 2912
+3666 and 1 3665 2915
+3667 ite 25 3666 26 1257
+3668 next 25 1257 3667
+3669 and 1 2982 3254
+3670 and 1 3669 2915
+3671 ite 25 3670 26 1258
+3672 next 25 1258 3671
+3673 and 1 2987 3254
+3674 and 1 3673 2915
+3675 ite 25 3674 26 1259
+3676 next 25 1259 3675
+3677 and 1 2921 2911
+3678 and 1 2901 3677
+3679 and 1 3678 2915
+3680 ite 25 3679 26 1260
+3681 next 25 1260 3680
+3682 and 1 2998 3677
+3683 and 1 3682 2915
+3684 ite 25 3683 26 1261
+3685 next 25 1261 3684
+3686 and 1 3003 3677
+3687 and 1 3686 2915
+3688 ite 25 3687 26 1262
+3689 next 25 1262 3688
+3690 and 1 3008 3677
+3691 and 1 3690 2915
+3692 ite 25 3691 26 1263
+3693 next 25 1263 3692
+3694 and 1 2920 3677
+3695 and 1 3694 2915
+3696 ite 25 3695 26 1264
+3697 next 25 1264 3696
+3698 and 1 2929 3677
+3699 and 1 3698 2915
+3700 ite 25 3699 26 1265
+3701 next 25 1265 3700
+3702 and 1 2935 3677
+3703 and 1 3702 2915
+3704 ite 25 3703 26 1266
+3705 next 25 1266 3704
+3706 and 1 2941 3677
+3707 and 1 3706 2915
+3708 ite 25 3707 26 1267
+3709 next 25 1267 3708
+3710 and 1 3008 2912
+3711 and 1 3710 2915
+3712 ite 25 3711 26 1268
+3713 next 25 1268 3712
+3714 and 1 2947 3677
+3715 and 1 3714 2915
+3716 ite 25 3715 26 1269
+3717 next 25 1269 3716
+3718 and 1 2952 3677
+3719 and 1 3718 2915
+3720 ite 25 3719 26 1270
+3721 next 25 1270 3720
+3722 and 1 2957 3677
+3723 and 1 3722 2915
+3724 ite 25 3723 26 1271
+3725 next 25 1271 3724
+3726 and 1 2962 3677
+3727 and 1 3726 2915
+3728 ite 25 3727 26 1272
+3729 next 25 1272 3728
+3730 and 1 2968 3677
+3731 and 1 3730 2915
+3732 ite 25 3731 26 1273
+3733 next 25 1273 3732
+3734 and 1 2973 3677
+3735 and 1 3734 2915
+3736 ite 25 3735 26 1274
+3737 next 25 1274 3736
+3738 and 1 2982 3677
+3739 and 1 3738 2915
+3740 ite 25 3739 26 1275
+3741 next 25 1275 3740
+3742 and 1 2987 3677
+3743 and 1 3742 2915
+3744 ite 25 3743 26 1276
+3745 next 25 1276 3744
+3746 and 1 2992 2911
+3747 and 1 2901 3746
+3748 and 1 3747 2915
+3749 ite 25 3748 26 1277
+3750 next 25 1277 3749
+3751 and 1 2998 3746
+3752 and 1 3751 2915
+3753 ite 25 3752 26 1278
+3754 next 25 1278 3753
+3755 and 1 2920 2912
+3756 and 1 3755 2915
+3757 ite 25 3756 26 1279
+3758 next 25 1279 3757
+3759 and 1 3003 3746
+3760 and 1 3759 2915
+3761 ite 25 3760 26 1280
+3762 next 25 1280 3761
+3763 and 1 3008 3746
+3764 and 1 3763 2915
+3765 ite 25 3764 26 1281
+3766 next 25 1281 3765
+3767 and 1 2920 3746
+3768 and 1 3767 2915
+3769 ite 25 3768 26 1282
+3770 next 25 1282 3769
+3771 and 1 2929 3746
+3772 and 1 3771 2915
+3773 ite 25 3772 26 1283
+3774 next 25 1283 3773
+3775 and 1 2935 3746
+3776 and 1 3775 2915
+3777 ite 25 3776 26 1284
+3778 next 25 1284 3777
+3779 and 1 2941 3746
+3780 and 1 3779 2915
+3781 ite 25 3780 26 1285
+3782 next 25 1285 3781
+3783 and 1 2947 3746
+3784 and 1 3783 2915
+3785 ite 25 3784 26 1286
+3786 next 25 1286 3785
+3787 and 1 2952 3746
+3788 and 1 3787 2915
+3789 ite 25 3788 26 1287
+3790 next 25 1287 3789
+3791 and 1 2957 3746
+3792 and 1 3791 2915
+3793 ite 25 3792 26 1288
+3794 next 25 1288 3793
+3795 and 1 2962 3746
+3796 and 1 3795 2915
+3797 ite 25 3796 26 1289
+3798 next 25 1289 3797
+3799 and 1 2929 2912
+3800 and 1 3799 2915
+3801 ite 25 3800 26 1290
+3802 next 25 1290 3801
+3803 and 1 2968 3746
+3804 and 1 3803 2915
+3805 ite 25 3804 26 1291
+3806 next 25 1291 3805
+3807 and 1 2973 3746
+3808 and 1 3807 2915
+3809 ite 25 3808 26 1292
+3810 next 25 1292 3809
+3811 and 1 2982 3746
+3812 and 1 3811 2915
+3813 ite 25 3812 26 1293
+3814 next 25 1293 3813
+3815 and 1 2987 3746
+3816 and 1 3815 2915
+3817 ite 25 3816 26 1294
+3818 next 25 1294 3817
+3819 and 1 2906 2922
+3820 and 1 2901 3819
+3821 and 1 3820 2915
+3822 ite 25 3821 26 1295
+3823 next 25 1295 3822
+3824 and 1 2998 3819
+3825 and 1 3824 2915
+3826 ite 25 3825 26 1296
+3827 next 25 1296 3826
+3828 and 1 3003 3819
+3829 and 1 3828 2915
+3830 ite 25 3829 26 1297
+3831 next 25 1297 3830
+3832 and 1 3008 3819
+3833 and 1 3832 2915
+3834 ite 25 3833 26 1298
+3835 next 25 1298 3834
+3836 and 1 2920 3819
+3837 and 1 3836 2915
+3838 ite 25 3837 26 1299
+3839 next 25 1299 3838
+3840 and 1 2929 3819
+3841 and 1 3840 2915
+3842 ite 25 3841 26 1300
+3843 next 25 1300 3842
+3844 and 1 2935 2912
+3845 and 1 3844 2915
+3846 ite 25 3845 26 1301
+3847 next 25 1301 3846
+3848 and 1 2935 3819
+3849 and 1 3848 2915
+3850 ite 25 3849 26 1302
+3851 next 25 1302 3850
+3852 and 1 2941 3819
+3853 and 1 3852 2915
+3854 ite 25 3853 26 1303
+3855 next 25 1303 3854
+3856 and 1 2947 3819
+3857 and 1 3856 2915
+3858 ite 25 3857 26 1304
+3859 next 25 1304 3858
+3860 and 1 2952 3819
+3861 and 1 3860 2915
+3862 ite 25 3861 26 1305
+3863 next 25 1305 3862
+3864 and 1 2957 3819
+3865 and 1 3864 2915
+3866 ite 25 3865 26 1306
+3867 next 25 1306 3866
+3868 and 1 2962 3819
+3869 and 1 3868 2915
+3870 ite 25 3869 26 1307
+3871 next 25 1307 3870
+3872 and 1 2968 3819
+3873 and 1 3872 2915
+3874 ite 25 3873 26 1308
+3875 next 25 1308 3874
+3876 and 1 2973 3819
+3877 and 1 3876 2915
+3878 ite 25 3877 26 1309
+3879 next 25 1309 3878
+3880 and 1 2982 3819
+3881 and 1 3880 2915
+3882 ite 25 3881 26 1310
+3883 next 25 1310 3882
+3884 and 1 2987 3819
+3885 and 1 3884 2915
+3886 ite 25 3885 26 1311
+3887 next 25 1311 3886
+3888 and 1 2941 2912
+3889 and 1 3888 2915
+3890 ite 25 3889 26 1312
+3891 next 25 1312 3890
+3892 and 1 3139 2922
+3893 and 1 2901 3892
+3894 and 1 3893 2915
+3895 ite 25 3894 26 1313
+3896 next 25 1313 3895
+3897 and 1 2998 3892
+3898 and 1 3897 2915
+3899 ite 25 3898 26 1314
+3900 next 25 1314 3899
+3901 and 1 3003 3892
+3902 and 1 3901 2915
+3903 ite 25 3902 26 1315
+3904 next 25 1315 3903
+3905 and 1 3008 3892
+3906 and 1 3905 2915
+3907 ite 25 3906 26 1316
+3908 next 25 1316 3907
+3909 and 1 2920 3892
+3910 and 1 3909 2915
+3911 ite 25 3910 26 1317
+3912 next 25 1317 3911
+3913 and 1 2929 3892
+3914 and 1 3913 2915
+3915 ite 25 3914 26 1318
+3916 next 25 1318 3915
+3917 and 1 2935 3892
+3918 and 1 3917 2915
+3919 ite 25 3918 26 1319
+3920 next 25 1319 3919
+3921 and 1 2941 3892
+3922 and 1 3921 2915
+3923 ite 25 3922 26 1320
+3924 next 25 1320 3923
+3925 and 1 2947 3892
+3926 and 1 3925 2915
+3927 ite 25 3926 26 1321
+3928 next 25 1321 3927
+3929 and 1 2952 3892
+3930 and 1 3929 2915
+3931 ite 25 3930 26 1322
+3932 next 25 1322 3931
+3933 and 1 2947 2912
+3934 and 1 3933 2915
+3935 ite 25 3934 26 1323
+3936 next 25 1323 3935
+3937 and 1 2957 3892
+3938 and 1 3937 2915
+3939 ite 25 3938 26 1324
+3940 next 25 1324 3939
+3941 and 1 2962 3892
+3942 and 1 3941 2915
+3943 ite 25 3942 26 1325
+3944 next 25 1325 3943
+3945 and 1 2968 3892
+3946 and 1 3945 2915
+3947 ite 25 3946 26 1326
+3948 next 25 1326 3947
+3949 and 1 2973 3892
+3950 and 1 3949 2915
+3951 ite 25 3950 26 1327
+3952 next 25 1327 3951
+3953 and 1 2982 3892
+3954 and 1 3953 2915
+3955 ite 25 3954 26 1328
+3956 next 25 1328 3955
+3957 and 1 2987 3892
+3958 and 1 3957 2915
+3959 ite 25 3958 26 1329
+3960 next 25 1329 3959
+3961 and 1 2901 2923
+3962 and 1 3961 2915
+3963 ite 25 3962 26 1330
+3964 next 25 1330 3963
+3965 and 1 2998 2923
+3966 and 1 3965 2915
+3967 ite 25 3966 26 1331
+3968 next 25 1331 3967
+3969 and 1 3003 2923
+3970 and 1 3969 2915
+3971 ite 25 3970 26 1332
+3972 next 25 1332 3971
+3973 and 1 3008 2923
+3974 and 1 3973 2915
+3975 ite 25 3974 26 1333
+3976 next 25 1333 3975
+3977 and 1 2952 2912
+3978 and 1 3977 2915
+3979 ite 25 3978 26 1334
+3980 next 25 1334 3979
+3981 ite 28 2267 1339 1337
+3982 ite 28 78 3981 1337
+3983 ite 28 2272 3982 1337
+3984 ite 28 2250 33 1337
+3985 ite 28 2300 3984 3983
+3986 ite 28 2281 3985 1337
+3987 ite 28 80 3986 1337
+3988 ite 28 1349 1337 3987
+3989 ite 28 20 3988 2089
+3990 next 28 1337 3989
+3991 slice 28 1078 23 16
+3992 uext 25 3991 1
+3993 eq 1 269 3992
+3994 ite 17 3993 2252 593
+3995 ite 17 2099 3994 593
+3996 slice 28 1078 15 8
+3997 uext 25 3996 1
+3998 eq 1 269 3997
+3999 ite 17 3998 2098 593
+4000 ite 17 2101 3999 3995
+4001 slice 28 1078 7 0
+4002 uext 25 4001 1
+4003 eq 1 269 4002
+4004 ite 17 4003 2100 593
+4005 ite 17 2103 4004 4000
+4006 ite 17 257 593 1344
+4007 ite 17 2879 2102 4006
+4008 ite 17 2106 4007 4005
+4009 neq 1 269 2082
+4010 and 1 257 4009
+4011 neq 1 269 2066
+4012 and 1 4010 4011
+4013 neq 1 269 2068
+4014 and 1 4012 4013
+4015 ite 17 4014 593 1344
+4016 ite 17 2879 2102 4015
+4017 const 17 0110
+4018 ite 17 2882 4017 4016
+4019 ite 17 2109 4018 4008
+4020 ite 260 257 857 2107
+4021 concat 17 9 4020
+4022 ite 17 2112 4021 4019
+4023 ite 258 257 2699 2110
+4024 concat 17 2699 4023
+4025 ite 17 2115 4024 4022
+4026 ite 17 841 593 1344
+4027 const 28 10011110
+4028 uext 25 4027 1
+4029 eq 1 269 4028
+4030 ite 17 4029 2755 4026
+4031 ite 17 2117 4030 4025
+4032 ite 17 2119 1344 4031
+4033 const 17 0001
+4034 ite 17 2130 4033 4032
+4035 ite 17 842 593 4034
+4036 ite 17 2137 4035 1344
+4037 ite 17 80 593 4036
+4038 ite 17 20 4037 593
+4039 next 17 1344 4038
+4040 ite 28 2250 2089 1345
+4041 ite 28 2296 4040 1345
+4042 ite 28 2281 4041 1345
+4043 ite 28 80 4042 1345
+4044 ite 28 1349 1345 4043
+4045 ite 28 20 4044 2089
+4046 next 28 1345 4045
+4047 ite 28 2250 1337 1346
+4048 ite 28 2296 4047 1346
+4049 ite 28 2281 4048 1346
+4050 ite 28 80 4049 1346
+4051 ite 28 1349 1346 4050
+4052 ite 28 20 4051 2089
+4053 next 28 1346 4052
+4054 ite 17 63 1347 593
+4055 ite 17 2250 4054 1347
+4056 const 17 1110
+4057 ite 17 2250 4056 1347
+4058 ite 17 2291 4057 4055
+4059 ite 17 2250 2290 1347
+4060 ite 17 2293 4059 4058
+4061 ite 17 2250 2292 1347
+4062 ite 17 2253 4061 4060
+4063 ite 17 2250 2252 1347
+4064 ite 17 2254 4063 4062
+4065 ite 17 2250 2098 1347
+4066 ite 17 2255 4065 4064
+4067 ite 17 2250 2100 1347
+4068 ite 17 2256 4067 4066
+4069 ite 17 2250 2102 1347
+4070 ite 17 2296 4069 4068
+4071 const 17 0111
+4072 ite 17 2250 4071 1347
+4073 ite 17 2298 4072 4070
+4074 ite 17 2414 4071 2100
+4075 ite 17 2267 1347 4074
+4076 ite 17 2250 4075 1347
+4077 ite 17 2272 4076 4073
+4078 ite 17 2414 4017 2102
+4079 const 17 0101
+4080 neq 1 29 33
+4081 ite 17 4080 4079 4078
+4082 ite 17 2250 4081 1347
+4083 ite 17 2300 4082 4077
+4084 const 17 0100
+4085 ite 17 2250 4084 1347
+4086 ite 17 2302 4085 4083
+4087 const 17 0011
+4088 ite 17 2250 4087 1347
+4089 ite 17 2304 4088 4086
+4090 ite 17 2250 2755 1347
+4091 ite 17 2306 4090 4089
+4092 ite 17 2250 4033 1347
+4093 ite 17 2276 4092 4091
+4094 ite 17 2281 4093 1347
+4095 ite 17 80 4094 593
+4096 ite 17 1349 593 4095
+4097 ite 17 20 4096 593
+4098 next 17 1347 4097
+4099 const 266 0000000
+4100 uext 266 30 6
+4101 add 266 1348 4100
+4102 ite 266 2267 4101 1348
+4103 ite 266 2250 4102 1348
+4104 ite 266 2272 4103 1348
+4105 ite 266 2250 4099 1348
+4106 ite 266 2300 4105 4104
+4107 ite 266 2281 4106 1348
+4108 ite 266 80 4107 1348
+4109 ite 266 2326 4101 1348
+4110 ite 266 2328 4109 1348
+4111 ite 266 1349 4110 4108
+4112 ite 266 20 4111 4099
+4113 next 266 1348 4112
+4114 ite 1 2328 2327 30
+4115 ite 1 1349 4114 9
+4116 ite 1 20 4115 30
+4117 next 1 1349 4116
+4118 concat 258 161 148
+4119 concat 260 168 4118
+4120 concat 17 173 4119
+4121 concat 57 181 4120
+4122 concat 264 208 4121
+4123 concat 266 219 4122
+4124 concat 28 243 4123
+4125 ite 28 2115 4124 1355
+4126 ite 28 2130 1355 4125
+4127 ite 28 842 1355 4126
+4128 ite 28 2137 4127 1355
+4129 ite 28 80 1355 4128
+4130 ite 28 20 4129 1355
+4131 next 28 1355 4130
+4132 concat 25 9 1345
+4133 eq 1 1355 1346
+4134 neq 1 1355 33
+4135 and 1 4133 4134
+4136 ite 25 4135 4132 1011
+4137 uext 25 1345 1
+4138 neq 1 1362 4137
+4139 ite 25 4138 4136 1362
+4140 ite 25 2096 4139 1362
+4141 ite 25 2128 1362 4140
+4142 ite 25 2130 1362 4141
+4143 ite 25 842 1362 4142
+4144 ite 25 2137 4143 1362
+4145 ite 25 80 1362 4144
+4146 ite 25 20 4145 1011
+4147 next 25 1362 4146
+4148 eq 1 1369 43
+4149 not 1 1367
+4150 or 1 4148 4149
+4151 ite 28 4150 1366 1369
+4152 ite 28 4014 1366 4151
+4153 ite 28 2879 1366 4152
+4154 ite 28 2882 1366 4153
+4155 ite 28 2109 4154 1366
+4156 ite 28 4029 42 1366
+4157 ite 28 2117 4156 4155
+4158 ite 28 2130 1366 4157
+4159 ite 28 842 1366 4158
+4160 ite 28 2137 4159 1366
+4161 ite 28 80 1366 4160
+4162 ite 28 20 4161 1366
+4163 next 28 1366 4162
+4164 ite 1 4150 9 1367
+4165 ite 1 4014 1367 4164
+4166 ite 1 2879 1367 4165
+4167 ite 1 2882 1367 4166
+4168 ite 1 2109 4167 1367
+4169 uext 25 1366 1
+4170 eq 1 269 4169
+4171 ite 1 2112 4170 4168
+4172 ite 1 2130 1367 4171
+4173 ite 1 842 1367 4172
+4174 ite 1 2137 4173 1367
+4175 ite 1 80 1367 4174
+4176 ite 1 20 4175 1367
+4177 next 1 1367 4176
+4178 slice 2026 1376 226 0
+4179 concat 1374 4178 4
+4180 next 1374 1376 4179
+; end of yosys output
diff --git a/test/regress/parser/btor2/ponylink-slaveTXlen-sat.btor2.options b/test/regress/parser/btor2/ponylink-slaveTXlen-sat.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/ponylink-slaveTXlen-sat.btor2.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/recount4.btor2 b/test/regress/parser/btor2/recount4.btor2
new file mode 100644
index 00000000..c644af15
--- /dev/null
+++ b/test/regress/parser/btor2/recount4.btor2
@@ -0,0 +1,15 @@
+1 sort bitvec 1
+2 input 1 enable
+3 input 1 reset
+4 sort bitvec 4
+5 zero 4
+6 state 4 counter
+7 init 4 6 5
+8 one 4
+9 add 4 6 8
+10 ite 4 2 9 6
+11 ite 4 3 5 10
+12 next 4 6 11
+13 ones 4
+14 eq 1 6 13
+15 bad 14
diff --git a/test/regress/parser/btor2/recount4.btor2.options b/test/regress/parser/btor2/recount4.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/recount4.btor2.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/twocount2.btor2 b/test/regress/parser/btor2/twocount2.btor2
new file mode 100644
index 00000000..c5ba40e6
--- /dev/null
+++ b/test/regress/parser/btor2/twocount2.btor2
@@ -0,0 +1,20 @@
+1 sort bitvec 1
+2 sort bitvec 2
+3 input 1 turn
+4 zero 2
+5 state 2 a
+6 state 2 b
+7 init 2 5 4
+8 init 2 6 4
+9 one 2
+10 add 2 5 9
+11 add 2 6 9
+12 ite 2 3 5 10
+13 ite 2 -3 6 11
+14 next 2 5 12
+15 next 2 6 13
+16 ones 2
+17 eq 1 5 16
+18 eq 1 6 16
+19 and 1 17 18
+20 bad 19
diff --git a/test/regress/parser/btor2/twocount2.btor2.options b/test/regress/parser/btor2/twocount2.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/twocount2.btor2.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/twocount2c.btor2 b/test/regress/parser/btor2/twocount2c.btor2
new file mode 100644
index 00000000..dee38515
--- /dev/null
+++ b/test/regress/parser/btor2/twocount2c.btor2
@@ -0,0 +1,23 @@
+1 sort bitvec 1
+2 sort bitvec 2
+3 input 1 s
+4 input 1 t
+5 zero 2
+6 state 2 a
+7 state 2 b
+8 init 2 6 5
+9 init 2 7 5
+10 one 2
+11 add 2 6 10
+12 add 2 7 10
+13 ite 2 3 11 6
+14 ite 2 4 12 7
+15 next 2 6 13
+16 next 2 7 14
+17 ones 2
+18 eq 1 6 17
+19 eq 1 7 17
+20 and 1 18 19
+21 bad 20
+22 nand 1 3 4
+23 constraint 22
diff --git a/test/regress/parser/btor2/twocount2c.btor2.options b/test/regress/parser/btor2/twocount2c.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/twocount2c.btor2.options
@@ -0,0 +1 @@
+--parse-only
diff --git a/test/regress/parser/btor2/twocount32.btor2 b/test/regress/parser/btor2/twocount32.btor2
new file mode 100644
index 00000000..e8010dbf
--- /dev/null
+++ b/test/regress/parser/btor2/twocount32.btor2
@@ -0,0 +1,20 @@
+ 1 sort bitvec 1
+ 2 sort bitvec 32
+ 3 input 1 turn
+ 4 zero 2
+ 5 state 2 a
+ 6 state 2 b
+ 7 init 2 5 4
+ 8 init 2 6 4
+ 9 one 2
+10 add 2 5 9
+11 add 2 6 9
+12 ite 2 3 5 10
+13 ite 2 -3 6 11
+14 next 2 5 12
+15 next 2 6 13
+16 constd 2 3
+17 eq 1 5 16
+18 eq 1 6 16
+19 and 1 17 18
+20 bad 19
diff --git a/test/regress/parser/btor2/twocount32.btor2.options b/test/regress/parser/btor2/twocount32.btor2.options
new file mode 100644
index 00000000..bb8aee86
--- /dev/null
+++ b/test/regress/parser/btor2/twocount32.btor2.options
@@ -0,0 +1 @@
+--parse-only