Repository: stanford-centaur/pono (language: python)

Issue:
Prover update 1
first PR of the series.

It simplifies the prover class and also the inherited classes


Discussion / hints:

Fix patch:
diff --git a/CMakeLists.txt b/CMakeLists.txt
index c99ef0766..25800d93b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -137,7 +137,6 @@ set(SOURCES
   "${PROJECT_SOURCE_DIR}/core/ts.cpp"
   "${PROJECT_SOURCE_DIR}/core/rts.cpp"
   "${PROJECT_SOURCE_DIR}/core/fts.cpp"
-  "${PROJECT_SOURCE_DIR}/core/prop.cpp"
   "${PROJECT_SOURCE_DIR}/core/unroller.cpp"
   "${PROJECT_SOURCE_DIR}/core/adaptive_unroller.cpp"
   "${PROJECT_SOURCE_DIR}/core/functional_unroller.cpp"
diff --git a/core/prop.cpp b/core/prop.cpp
deleted file mode 100644
index 83ba1c59b..000000000
--- a/core/prop.cpp
+++ /dev/null
@@ -1,102 +0,0 @@
-/*********************                                                        */
-/*! \file
- ** \verbatim
- ** Top contributors (to current version):
- **   Ahmed Irfan, Makai Mann
- ** This file is part of the pono project.
- ** Copyright (c) 2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file LICENSE in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief
- **
- **
- **/
-
-#include "core/prop.h"
-
-#include "assert.h"
-#include "core/rts.h"
-#include "smt-switch/utils.h"
-#include "utils/exceptions.h"
-#include "utils/logger.h"
-
-using namespace smt;
-
-namespace pono {
-
-Property::Property(const TransitionSystem & ts, const Term & p,
-                   std::string name)
-  : ts_(ts), prop_(p), name_(name)
-{
-  // find a name if it wasn't provided
-  // if no name is associated with it in the ts, then it will just
-  // be the to_string of the term
-  if (name_.empty())
-  {
-    name_ = ts_.get_name(prop_);
-  }
-  initialize();
-}
-
-Property::Property(Property & prop, TermTranslator & tt)
-    : ts_(prop.ts_, tt),
-      // only need to transfer if solvers are different
-      // ts_ constructor does the same thing internally
-      prop_((prop.transition_system().solver() == tt.get_solver())
-                ? prop.prop_
-                : tt.transfer_term(prop.prop_, BOOL)),
-      name_(prop.name_)
-{
-}
-
-Property::~Property() {}
-
-void Property::initialize()
-{
-  if (ts_.only_curr(prop_)) {
-    // nothing to do
-    return;
-  }
-
-  // otherwise, need to make sure prop_ is over state vars
-  logger.log(1,
-             "Got next state or input variables in property. Generating a "
-             "monitor state.");
-
-  Term monitor;
-  size_t id = 0;
-  while (true) {
-    try {
-      monitor = ts_.make_statevar("_monitor_" + std::to_string(id),
-                                  ts_.make_sort(BOOL));
-      break;
-    }
-    catch (SmtException & e) {
-      ++id;
-    }
-  }
-  assert(monitor);
-
-  // monitor starts true
-  ts_.constrain_init(monitor);
-
-  if (ts_.no_next(prop_)) {
-    ts_.assign_next(monitor, prop_);
-
-  } else if (!ts_.is_functional()) {
-    RelationalTransitionSystem & rts =
-        static_cast<RelationalTransitionSystem &>(ts_);
-    rts.constrain_trans(rts.make_term(Equal, rts.next(monitor), prop_));
-  } else {
-    assert(ts_.is_functional());
-    throw PonoException(
-        "Cannot use next in property of a functional transition system.");
-  }
-
-  // update prop_
-  prop_ = monitor;
-}
-
-}  // namespace pono
diff --git a/core/prop.h b/core/prop.h
index 8490b5bc0..6bab0eb20 100644
--- a/core/prop.h
+++ b/core/prop.h
@@ -24,28 +24,21 @@ namespace pono {
 class Property
 {
  public:
-  Property(const TransitionSystem & ts, const smt::Term & p,
-           std::string name="");
+  Property(const smt::SmtSolver & s, const smt::Term & p,
+           std::string name="")
+    : solver_(s), prop_(p), name_(name)
+  {};
 
-  /** Copies property to a new solver
-   *  @param prop the property to copy
-   *  @param tt the term translator to use
-   *  @return a property using the solver in tt
-   */
-  Property(Property & prop, smt::TermTranslator & tt);
+  ~Property() {};
 
-  ~Property();
+  const smt::Term & prop() const { return prop_; }
 
-  const smt::Term prop() const { return prop_; }
-
-  TransitionSystem & transition_system() { return ts_; }
+  const smt::SmtSolver & solver() const { return solver_; }
 
   std::string name() { return name_; };
 
  private:
-  void initialize();
-
-  TransitionSystem ts_;
+  smt::SmtSolver solver_;
 
   smt::Term prop_;
 
diff --git a/engines/bmc.cpp b/engines/bmc.cpp
index 756f795a6..ec34b217f 100644
--- a/engines/bmc.cpp
+++ b/engines/bmc.cpp
@@ -21,8 +21,9 @@ using namespace smt;
 
 namespace pono {
 
-Bmc::Bmc(Property & p, const SmtSolver & solver, PonoOptions opt)
-  : super(p, solver, opt)
+Bmc::Bmc(const Property & p, const TransitionSystem & ts,
+         const SmtSolver & solver, PonoOptions opt)
+  : super(p, ts, solver, opt)
 {
 }
 
@@ -35,12 +36,13 @@ void Bmc::initialize()
   }
 
   super::initialize();
+
   // NOTE: There's an implicit assumption that this solver is only used for
   // model checking once Otherwise there could be conflicting assertions to
   // the solver or it could just be polluted with redundant assertions in the
   // future we can use solver_->reset_assertions(), but it is not currently
   // supported in boolector
-  solver_->assert_formula(unroller_.at_time(ts_->init(), 0));
+  solver_->assert_formula(unroller_.at_time(ts_.init(), 0));
 }
 
 ProverResult Bmc::check_until(int k)
@@ -64,7 +66,7 @@ bool Bmc::step(int i)
 
   bool res = true;
   if (i > 0) {
-    solver_->assert_formula(unroller_.at_time(ts_->trans(), i - 1));
+    solver_->assert_formula(unroller_.at_time(ts_.trans(), i - 1));
   }
 
   solver_->push();
diff --git a/engines/bmc.h b/engines/bmc.h
index e7ffc714d..d7666e612 100644
--- a/engines/bmc.h
+++ b/engines/bmc.h
@@ -22,8 +22,9 @@ namespace pono {
 
 class Bmc : public Prover
 {
- public:
-  Bmc(Property & p, const smt::SmtSolver & solver,
+public:
+  Bmc(const Property & p, const TransitionSystem & ts,
+      const smt::SmtSolver & solver,
       PonoOptions opt = PonoOptions());
 
   ~Bmc();
@@ -34,7 +35,7 @@ class Bmc : public Prover
 
   ProverResult check_until(int k) override;
 
- private:
+ protected:
   bool step(int i);
 
 };  // class Bmc
diff --git a/engines/bmc_simplepath.cpp b/engines/bmc_simplepath.cpp
index 386f0cb2c..3300b3f75 100644
--- a/engines/bmc_simplepath.cpp
+++ b/engines/bmc_simplepath.cpp
@@ -22,9 +22,10 @@ using namespace smt;
 
 namespace pono {
 
-BmcSimplePath::BmcSimplePath(Property & p, const SmtSolver & solver,
+BmcSimplePath::BmcSimplePath(const Property & p, const TransitionSystem & ts,
+                             const SmtSolver & solver,
                              PonoOptions opt)
-  : super(p, solver, opt)
+  : super(p, ts, solver, opt)
 {
 }
 
@@ -56,11 +57,11 @@ bool BmcSimplePath::cover_step(int i)
 
   solver_->push();
   solver_->assert_formula(init0_);
-  Term not_init = solver_->make_term(PrimOp::Not, ts_->init());
+  Term not_init = solver_->make_term(PrimOp::Not, ts_.init());
   for (int j = 1; j <= i; ++j) {
     solver_->assert_formula(unroller_.at_time(not_init, j));
   }
-  if (ts_->statevars().size() && check_simple_path_lazy(i)) {
+  if (ts_.statevars().size() && check_simple_path_lazy(i)) {
     return true;
   }
   solver_->pop();
diff --git a/engines/bmc_simplepath.h b/engines/bmc_simplepath.h
index dbe2dbd5c..e9053be92 100644
--- a/engines/bmc_simplepath.h
+++ b/engines/bmc_simplepath.h
@@ -23,7 +23,8 @@ namespace pono {
 class BmcSimplePath : public KInduction
 {
  public:
-  BmcSimplePath(Property & p, const smt::SmtSolver & solver,
+  BmcSimplePath(const Property & p, const TransitionSystem & ts,
+                const smt::SmtSolver & solver,
                 PonoOptions opt = PonoOptions());
 
   ~BmcSimplePath();
@@ -32,7 +33,7 @@ class BmcSimplePath : public KInduction
 
   ProverResult check_until(int k) override;
 
- private:
+ protected:
   bool cover_step(int i);
 
 };  // BmcSimplePath
diff --git a/engines/ceg_prophecy_arrays.cpp b/engines/ceg_prophecy_arrays.cpp
index 1e95610ac..1cfda6c65 100644
--- a/engines/ceg_prophecy_arrays.cpp
+++ b/engines/ceg_prophecy_arrays.cpp
@@ -31,21 +31,26 @@ using namespace std;
 
 namespace pono {
 
-CegProphecyArrays::CegProphecyArrays(Property & p,
+CegProphecyArrays::CegProphecyArrays(const Property & p,
+                                     const TransitionSystem & ts,
                                      Engine e,
                                      const SmtSolver & solver,
                                      PonoOptions opt)
-    : super(p, solver, opt),
-      conc_ts_(p.transition_system()),
-      solver_(conc_ts_.solver()),
-      abs_ts_(solver_),
+    : super(p, RelationalTransitionSystem(solver), solver, opt),
+      conc_ts_(ts),
       e_(e),
-      abs_unroller_(abs_ts_, solver_),
-      aa_(conc_ts_, abs_ts_, true),
-      aae_(aa_, abs_unroller_, p.prop(), options_.cegp_axiom_red_),
-      pm_(abs_ts_),
+      abs_unroller_(ts_, solver_),
+      aa_(conc_ts_, ts_, true),
+      aae_(aa_, abs_unroller_,
+           orig_ts_.solver() == solver_
+           ? p.prop()
+           : to_prover_solver_.transfer_term(p.prop()),
+           options_.cegp_axiom_red_),
+      pm_(ts_),
       num_added_axioms_(0)
 {
+  // point orig_ts_ to the correct one
+  orig_ts_ = ts;
 }
 
 ProverResult CegProphecyArrays::prove()
@@ -64,17 +69,11 @@ ProverResult CegProphecyArrays::prove()
       reached_k_++;
     } while (num_added_axioms_);
 
-    Property latest_prop(abs_ts_, solver_->make_term(Not, bad_));
-    PonoOptions opts = options_;
-    // disable static coi because it can't be called more than once on the same
-    // system
-    // TODO: handle this in a better way
-    opts.static_coi_ = false;
-
+    Property latest_prop(solver_, solver_->make_term(Not, bad_));
     //TODO : think about making it use the same prover -- incrementally
     SmtSolver s = create_solver(solver_->get_solver_enum());
     shared_ptr<Prover> prover =
-      make_prover(e_, latest_prop, s, opts);
+      make_prover(e_, latest_prop, ts_, s, options_);
 
     res = prover->prove();
   }
@@ -97,7 +96,7 @@ ProverResult CegProphecyArrays::check_until(int k)
       reached_k_++;
     } while (num_added_axioms_ && reached_k_ <= k);
 
-    Property latest_prop(abs_ts_, solver_->make_term(Not, bad_));
+    Property latest_prop(solver_, solver_->make_term(Not, bad_));
     PonoOptions opts = options_;
     // disable static coi because it can't be called more than once on the same
     // system
@@ -105,8 +104,7 @@ ProverResult CegProphecyArrays::check_until(int k)
     opts.static_coi_ = false;
 
     SmtSolver s = create_solver(solver_->get_solver_enum());
-    shared_ptr<Prover> prover =
-        make_prover(e_, latest_prop, s, opts);
+    shared_ptr<Prover> prover = make_prover(e_, latest_prop, ts_, s, opts);
 
     res = prover->check_until(k);
   }
@@ -122,19 +120,19 @@ ProverResult CegProphecyArrays::check_until(int k)
 
 void CegProphecyArrays::initialize()
 {
-  super::initialize();
-
   abstract();
+  // call super initializer after abstraction
+  super::initialize();
 
   bool contains_arrays = false;
-  for (auto sv : conc_ts_.statevars()) {
+  for (const auto &sv : conc_ts_.statevars()) {
     if (sv->get_sort()->get_sort_kind() == ARRAY) {
       contains_arrays = true;
       break;
     }
   }
 
-  for (auto iv : conc_ts_.inputvars()) {
+  for (const auto &iv : conc_ts_.inputvars()) {
     if (iv->get_sort()->get_sort_kind() == ARRAY) {
       contains_arrays = true;
       break;
@@ -150,13 +148,16 @@ void CegProphecyArrays::abstract()
 {
   // the ArrayAbstractor already abstracted the transition system on
   // construction -- only need to abstract bad
-  bad_ = aa_.abstract(bad_);
+  Term prop_term = (ts_.solver() == orig_property_.solver())
+    ? orig_property_.prop()
+    : to_prover_solver_.transfer_term(orig_property_.prop());
+  bad_ = solver_->make_term(smt::PrimOp::Not, aa_.abstract(prop_term));
 
   // the abstract system should have all the same state and input variables
   // but abstracted
   // plus it will have some new variables for the witnesses and lambdas
-  assert(abs_ts_.statevars().size() >= conc_ts_.statevars().size());
-  assert(abs_ts_.inputvars().size() >= conc_ts_.inputvars().size());
+  assert(ts_.statevars().size() >= conc_ts_.statevars().size());
+  assert(ts_.inputvars().size() >= conc_ts_.inputvars().size());
 }
 
 bool CegProphecyArrays::refine()
@@ -187,7 +188,7 @@ bool CegProphecyArrays::refine()
       // needed for it to be unsat with all the nonconsecutive axioms
       // it will be updated again later anyway
       for (auto ax : consecutive_axioms) {
-        size_t max_k = abs_ts_.only_curr(ax) ? reached_k_ + 1 : reached_k_;
+        size_t max_k = ts_.only_curr(ax) ? reached_k_ + 1 : reached_k_;
         for (size_t k = 0; k <= max_k; ++k) {
           abs_bmc_formula = solver_->make_term(
               And, abs_bmc_formula, abs_unroller_.at_time(ax, k));
@@ -221,7 +222,7 @@ bool CegProphecyArrays::refine()
       Term idx = abs_unroller_.untime(timed_idx);
       // can't target a non-current state variable
       // because the target will appear in the updated property
-      assert(delay > 0 || abs_ts_.only_curr(idx));
+      assert(delay > 0 || ts_.only_curr(idx));
       proph_vars.push_back(pm_.get_proph(idx, delay));
     }
 
@@ -260,18 +261,19 @@ bool CegProphecyArrays::refine()
 
   // add consecutive axioms to the system
   // TODO: make sure we're adding current / next correctly
+  RelationalTransitionSystem &rts = static_cast<RelationalTransitionSystem &>(ts_); 
   for (auto ax : consecutive_axioms) {
     num_added_axioms_++;
     if (reached_k_ == -1) {
       // if only checking initial state
       // need to add to init
-      abs_ts_.constrain_init(ax);
+      rts.constrain_init(ax);
     }
 
-    abs_ts_.constrain_trans(ax);
-    if (abs_ts_.only_curr(ax)) {
+    rts.constrain_trans(ax);
+    if (rts.only_curr(ax)) {
       // add the next state version if it's an invariant over current state vars
-      abs_ts_.constrain_trans(abs_ts_.next(ax));
+      rts.constrain_trans(ts_.next(ax));
     }
   }
 
@@ -284,10 +286,10 @@ bool CegProphecyArrays::refine()
 // helpers
 Term CegProphecyArrays::get_bmc_formula(size_t b)
 {
-  Term abs_bmc_formula = abs_unroller_.at_time(abs_ts_.init(), 0);
+  Term abs_bmc_formula = abs_unroller_.at_time(ts_.init(), 0);
   for (int k = 0; k < b; ++k) {
     abs_bmc_formula = solver_->make_term(
-        And, abs_bmc_formula, abs_unroller_.at_time(abs_ts_.trans(), k));
+        And, abs_bmc_formula, abs_unroller_.at_time(ts_.trans(), k));
   }
   return solver_->make_term(
       And, abs_bmc_formula, abs_unroller_.at_time(bad_, b));
@@ -307,7 +309,7 @@ void CegProphecyArrays::reduce_consecutive_axioms(const Term & abs_bmc_formula,
   Term lbl;
   for (auto ax : consec_ax) {
     unrolled_ax = solver_->make_term(true);
-    size_t max_k = abs_ts_.only_curr(ax) ? reached_k_ + 1 : reached_k_;
+    size_t max_k = ts_.only_curr(ax) ? reached_k_ + 1 : reached_k_;
     for (size_t k = 0; k <= max_k; ++k) {
       unrolled_ax =
           solver_->make_term(And, unrolled_ax, abs_unroller_.at_time(ax, k));
diff --git a/engines/ceg_prophecy_arrays.h b/engines/ceg_prophecy_arrays.h
index 29ed189a1..658e1fa6d 100644
--- a/engines/ceg_prophecy_arrays.h
+++ b/engines/ceg_prophecy_arrays.h
@@ -33,7 +33,8 @@ class CegProphecyArrays : public CEGAR
   typedef CEGAR super;
 
  public:
-  CegProphecyArrays(Property & p,
+  CegProphecyArrays(const Property & p,
+                    const TransitionSystem & ts,
                     Engine e,
                     const smt::SmtSolver & solver,
                     PonoOptions opt = PonoOptions());
@@ -50,8 +51,7 @@ class CegProphecyArrays : public CEGAR
 
  protected:
   const TransitionSystem & conc_ts_;
-  const smt::SmtSolver & solver_;
-  RelationalTransitionSystem abs_ts_;
+
   Engine e_;
 
   // TODO: see if there's a better organization where we can re-use the same
diff --git a/engines/cegar.h b/engines/cegar.h
index 64e73ee28..fd2666df8 100644
--- a/engines/cegar.h
+++ b/engines/cegar.h
@@ -26,9 +26,10 @@ class CEGAR : public Prover
   typedef Prover super;
 
  public:
-  CEGAR(Property & p, const smt::SmtSolver & solver,
+  CEGAR(const Property & p, const TransitionSystem & ts,
+        const smt::SmtSolver & solver,
         PonoOptions opt = PonoOptions())
-    : super(p, solver)
+    : super(p, ts, solver)
   {
   }
 
diff --git a/engines/ic3.cpp b/engines/ic3.cpp
index 964ac40e4..2795672f6 100644
--- a/engines/ic3.cpp
+++ b/engines/ic3.cpp
@@ -27,23 +27,24 @@ namespace pono {
 
 /** IC3 Implementation */
 
-IC3::IC3(Property & p, const smt::SmtSolver & s, PonoOptions opt)
-  : super(p, s, opt)
+IC3::IC3(const Property & p, const TransitionSystem & ts,
+         const smt::SmtSolver & s, PonoOptions opt)
+  : super(p, ts, s, opt)
 {
   solver_->set_opt("produce-unsat-cores", "true");
 }
 
 IC3Formula IC3::get_model_ic3formula(TermVec * out_inputs,
-                                      TermVec * out_nexts) const
+                                     TermVec * out_nexts) const
 {
   // expecting all solving in IC3 to be done at context level > 0
   // so if we're getting a model we should not be at context 0
   assert(solver_context_);
 
-  const UnorderedTermSet & statevars = ts_->statevars();
+  const UnorderedTermSet & statevars = ts_.statevars();
   TermVec children;
   children.reserve(statevars.size());
-  for (const auto &sv : ts_->statevars()) {
+  for (const auto &sv : ts_.statevars()) {
     if (solver_->get_value(sv) == solver_true_) {
       children.push_back(sv);
     } else {
@@ -51,7 +52,7 @@ IC3Formula IC3::get_model_ic3formula(TermVec * out_inputs,
     }
 
     if (out_nexts) {
-      Term nv = ts_->next(sv);
+      Term nv = ts_.next(sv);
       if (solver_->get_value(nv) == solver_true_) {
         out_nexts->push_back(nv);
       } else {
@@ -61,7 +62,7 @@ IC3Formula IC3::get_model_ic3formula(TermVec * out_inputs,
   }
 
   if (out_inputs) {
-    for (const auto &iv : ts_->inputvars()) {
+    for (const auto &iv : ts_.inputvars()) {
       if (solver_->get_value(iv) == solver_true_) {
         out_inputs->push_back(iv);
       } else {
@@ -140,7 +141,7 @@ std::vector<IC3Formula> IC3::inductive_generalization(size_t i,
         bool_assump.clear();
         for (const auto &t : tmp) {
           l = label(t);
-          solver_->assert_formula(solver_->make_term(Implies, l, ts_->next(t)));
+          solver_->assert_formula(solver_->make_term(Implies, l, ts_.next(t)));
           bool_assump.push_back(l);
         }
 
@@ -197,7 +198,7 @@ IC3Formula IC3::generalize_predecessor(size_t i, const IC3Formula & c)
   // sat
   assert(i > 0);
 
-  const UnorderedTermSet & statevars = ts_->statevars();
+  const UnorderedTermSet & statevars = ts_.statevars();
   TermVec input_lits, next_lits;
   const IC3Formula & icf = get_model_ic3formula(&input_lits, &next_lits);
   const TermVec & cube_lits = icf.children;
@@ -209,12 +210,12 @@ IC3Formula IC3::generalize_predecessor(size_t i, const IC3Formula & c)
   }
 
   Term formula = make_and(input_lits);
-  if (ts_->is_deterministic()) {
+  if (ts_.is_deterministic()) {
     // NOTE: need to use full trans, not just trans_label_ here
     //       because we are passing it to the reducer_
-    formula = solver_->make_term(And, formula, ts_->trans());
+    formula = solver_->make_term(And, formula, ts_.trans());
     formula = solver_->make_term(
-        And, formula, solver_->make_term(Not, ts_->next(c.term)));
+        And, formula, solver_->make_term(Not, ts_.next(c.term)));
   } else {
     formula = solver_->make_term(And, formula, make_and(next_lits));
 
@@ -226,10 +227,10 @@ IC3Formula IC3::generalize_predecessor(size_t i, const IC3Formula & c)
     // the implication could be more efficient than iff so we want to leave it
     // that way
     Term pre_formula = get_frame_term(i - 1);
-    pre_formula = solver_->make_term(And, pre_formula, ts_->trans());
+    pre_formula = solver_->make_term(And, pre_formula, ts_.trans());
     pre_formula =
         solver_->make_term(And, pre_formula, solver_->make_term(Not, c.term));
-    pre_formula = solver_->make_term(And, pre_formula, ts_->next(c.term));
+    pre_formula = solver_->make_term(And, pre_formula, ts_.next(c.term));
     formula =
         solver_->make_term(And, formula, solver_->make_term(Not, pre_formula));
   }
@@ -254,14 +255,14 @@ IC3Formula IC3::generalize_predecessor(size_t i, const IC3Formula & c)
 void IC3::check_ts() const
 {
   const Sort &boolsort = solver_->make_sort(BOOL);
-  for (const auto &sv : ts_->statevars()) {
+  for (const auto &sv : ts_.statevars()) {
     if (sv->get_sort() != boolsort) {
       throw PonoException("Got non-boolean state variable in bit-level IC3: "
                           + sv->to_string());
     }
   }
 
-  for (const auto &iv : ts_->inputvars()) {
+  for (const auto &iv : ts_.inputvars()) {
     if (iv->get_sort() != boolsort) {
       throw PonoException("Got non-boolean input variable in bit-level IC3: "
                           + iv->to_string());
diff --git a/engines/ic3.h b/engines/ic3.h
index 36842e4cf..0ddbe10c0 100644
--- a/engines/ic3.h
+++ b/engines/ic3.h
@@ -21,7 +21,8 @@ namespace pono {
 class IC3 : public IC3Base
 {
  public:
-  IC3(Property & p, const smt::SmtSolver & s, PonoOptions opt = PonoOptions());
+  IC3(const Property & p, const TransitionSystem & ts,
+      const smt::SmtSolver & s, PonoOptions opt = PonoOptions());
 
   virtual ~IC3() {}
 
diff --git a/engines/ic3base.cpp b/engines/ic3base.cpp
index 0699e026f..feb95b645 100644
--- a/engines/ic3base.cpp
+++ b/engines/ic3base.cpp
@@ -60,8 +60,9 @@ static bool subsumes(const IC3Formula &a, const IC3Formula &b)
 
 /** IC3Base */
 
-IC3Base::IC3Base(Property & p, const SmtSolver & s, PonoOptions opt)
-    : super(p, s, opt),
+IC3Base::IC3Base(const Property & p, const TransitionSystem & ts,
+                 const SmtSolver & s, PonoOptions opt)
+    : super(p, ts, s, opt),
       reducer_(create_solver(s->get_solver_enum())),
       solver_context_(0),
       num_check_sat_since_reset_(0),
@@ -93,10 +94,6 @@ void IC3Base::initialize()
   // otherwise it is a No-Op
   abstract();
 
-  // ts_ should not only be set but also be the correct one at this point
-  // e.g. if abstracting, it now points to the abstract transition system
-  assert(ts_);
-
   // check whether this flavor of IC3 can be applied to this transition system
   check_ts();
 
@@ -108,7 +105,7 @@ void IC3Base::initialize()
   // can't use constrain_frame for initial states because not guaranteed to be
   // an IC3Formula it's handled specially
   solver_->assert_formula(
-      solver_->make_term(Implies, frame_labels_.at(0), ts_->init()));
+      solver_->make_term(Implies, frame_labels_.at(0), ts_.init()));
   push_frame();
 
   // set semantics of TS labels
@@ -119,7 +116,7 @@ void IC3Base::initialize()
   init_label_ = frame_labels_[0];
   trans_label_ = solver_->make_symbol("__trans_label", boolsort);
   solver_->assert_formula(
-      solver_->make_term(Implies, trans_label_, ts_->trans()));
+      solver_->make_term(Implies, trans_label_, ts_.trans()));
 }
 
 ProverResult IC3Base::check_until(int k)
@@ -343,7 +340,7 @@ bool IC3Base::rel_ind_check(size_t i,
   // Trans
   assert_trans_label();
   // c'
-  solver_->assert_formula(ts_->next(c.term));
+  solver_->assert_formula(ts_.next(c.term));
 
   Result r = check_sat();
   if (r.is_sat()) {
@@ -375,7 +372,7 @@ bool IC3Base::rel_ind_check(size_t i,
     for (const auto &u : out) {
       conj = solver_->make_term(And, conj, u.term);
       assert(ic3formula_check_valid(u));
-      assert(ts_->only_curr(u.term));
+      assert(ts_.only_curr(u.term));
     }
     assert(!check_intersects_initial(solver_->make_term(Not, conj)));
   }
@@ -539,7 +536,7 @@ bool IC3Base::propagate(size_t i)
     // Check F[i] /\ t /\ T /\ -t'
     // NOTE: asserting t is redundant because t \in F[i]
     push_solver_context();
-    solver_->assert_formula(solver_->make_term(Not, ts_->next(t)));
+    solver_->assert_formula(solver_->make_term(Not, ts_.next(t)));
 
     Result r = check_sat();
     assert(!r.is_unknown());
@@ -629,7 +626,7 @@ Term IC3Base::get_frame_term(size_t i) const
   //       need to special case initial state if using IC3Formulas
   if (i == 0) {
     // F[0] is always the initial states constraint
-    return ts_->init();
+    return ts_.init();
   }
 
   Term res = solver_true_;
@@ -685,7 +682,7 @@ void IC3Base::fix_if_intersects_initial(TermVec & to_keep, const TermVec & rem)
     // TODO: there's a tricky issue here. The reducer doesn't have the label
     // assumptions so we can't use init_label_ here. need to come up with a
     // better interface. Should we add label assumptions to reducer?
-    const Term &formula = solver_->make_term(And, ts_->init(), make_and(to_keep));
+    const Term &formula = solver_->make_term(And, ts_.init(), make_and(to_keep));
     reducer_.reduce_assump_unsatcore(formula,
                                      rem,
                                      to_keep,
@@ -701,7 +698,7 @@ size_t IC3Base::find_highest_frame(size_t i, const IC3Formula & u)
   const Term &c = u.term;
   push_solver_context();
   solver_->assert_formula(c);
-  solver_->assert_formula(solver_->make_term(Not, ts_->next(c)));
+  solver_->assert_formula(solver_->make_term(Not, ts_.next(c)));
   assert_trans_label();
 
   Result r;
@@ -759,9 +756,9 @@ void IC3Base::reset_solver()
     // define init and trans label
     assert(init_label_ == frame_labels_.at(0));
     solver_->assert_formula(
-        solver_->make_term(Implies, init_label_, ts_->init()));
+        solver_->make_term(Implies, init_label_, ts_.init()));
     solver_->assert_formula(
-        solver_->make_term(Implies, trans_label_, ts_->trans()));
+        solver_->make_term(Implies, trans_label_, ts_.trans()));
 
     for (size_t i = 0; i < frames_.size(); ++i) {
       for (const auto & constraint : frames_.at(i)) {
diff --git a/engines/ic3base.h b/engines/ic3base.h
index 797c0d7cc..4564580f3 100644
--- a/engines/ic3base.h
+++ b/engines/ic3base.h
@@ -174,7 +174,8 @@ class IC3Base : public Prover
    *  Depending on the derived class IC3 implementation, the exact
    *  type of IC3Formula will differ: e.g. Clause, Disjunction
    */
-  IC3Base(Property & p, const smt::SmtSolver & s,
+  IC3Base(const Property & p, const TransitionSystem & ts,
+          const smt::SmtSolver & s,
           PonoOptions opt = PonoOptions());
 
   virtual ~IC3Base();
diff --git a/engines/ic3ia.cpp b/engines/ic3ia.cpp
index e9cf2d7b3..6fd3fb6d6 100644
--- a/engines/ic3ia.cpp
+++ b/engines/ic3ia.cpp
@@ -40,12 +40,12 @@ using namespace std;
 
 namespace pono {
 
-IC3IA::IC3IA(Property & p, const SmtSolver & s, SmtSolver itp,
+IC3IA::IC3IA(const Property & p, const TransitionSystem & ts,
+             const SmtSolver & s, const SmtSolver & itp,
              PonoOptions opt)
-    : super(p, s, opt),
-      conc_ts_(property_.transition_system()),
-      abs_ts_(solver_),
-      ia_(conc_ts_, abs_ts_, unroller_),
+    : super(p, RelationalTransitionSystem(s), s, opt),
+      conc_ts_(ts, to_prover_solver_),
+      ia_(conc_ts_, ts_, unroller_),
       interpolator_(itp),
       to_interpolator_(interpolator_),
       to_solver_(solver_),
@@ -56,7 +56,7 @@ IC3IA::IC3IA(Property & p, const SmtSolver & s, SmtSolver itp,
 // pure virtual method implementations
 
 IC3Formula IC3IA::get_model_ic3formula(TermVec * out_inputs,
-                                        TermVec * out_nexts) const
+                                       TermVec * out_nexts) const
 {
   const TermVec & preds = ia_.predicates();
   TermVec conjuncts;
@@ -69,7 +69,7 @@ IC3Formula IC3IA::get_model_ic3formula(TermVec * out_inputs,
     }
 
     if (out_nexts) {
-      Term next_p = ts_->next(p);
+      Term next_p = ts_.next(p);
       if (solver_->get_value(next_p) == solver_true_) {
         out_nexts->push_back(next_p);
       } else {
@@ -79,7 +79,7 @@ IC3Formula IC3IA::get_model_ic3formula(TermVec * out_inputs,
   }
 
   if (out_inputs) {
-    for (const auto &iv : ts_->inputvars()) {
+    for (const auto &iv : ts_.inputvars()) {
       out_inputs->push_back(
           solver_->make_term(Equal, iv, solver_->get_value(iv)));
     }
@@ -133,7 +133,7 @@ void IC3IA::initialize()
   // add all the predicates from init and property to the abstraction
   // NOTE: abstract is called automatically in IC3Base initialize
   UnorderedTermSet preds;
-  get_predicates(solver_, ts_->init(), preds, true);
+  get_predicates(solver_, ts_.init(), preds, true);
   size_t num_init_preds = preds.size();
   get_predicates(solver_, bad_, preds, true);
   size_t num_prop_preds = preds.size() - num_init_preds;
@@ -150,12 +150,12 @@ void IC3IA::initialize()
   // populate cache for existing terms in solver_
   UnorderedTermMap & cache = to_solver_.get_cache();
   Term ns;
-  for (auto const&s : ts_->statevars()) {
+  for (auto const&s : ts_.statevars()) {
     // common variables are next states, unless used for refinement in IC3IA
     // then will refer to current state variables after untiming
     // need to cache both
     cache[to_interpolator_.transfer_term(s)] = s;
-    ns = ts_->next(s);
+    ns = ts_.next(s);
     cache[to_interpolator_.transfer_term(ns)] = ns;
   }
 
@@ -164,8 +164,8 @@ void IC3IA::initialize()
   // NOTE need to use get_free_symbols NOT get_free_symbolic_consts
   // because the latter ignores uninterpreted functions
   UnorderedTermSet free_symbols;
-  get_free_symbols(ts_->init(), free_symbols);
-  get_free_symbols(ts_->trans(), free_symbols);
+  get_free_symbols(ts_.init(), free_symbols);
+  get_free_symbols(ts_.trans(), free_symbols);
   get_free_symbols(bad_, free_symbols);
 
   for (auto const&s : free_symbols) {
@@ -193,9 +193,8 @@ void IC3IA::abstract()
 {
   // main abstraction already done in constructor of ia_
   // just need to set ts_ to the abstraction
-  assert(abs_ts_.init());  // should be non-null
-  assert(abs_ts_.trans());
-  ts_ = &abs_ts_;
+  assert(ts_.init());  // should be non-null
+  assert(ts_.trans());
 }
 
 RefineResult IC3IA::refine()
@@ -207,7 +206,7 @@ RefineResult IC3IA::refine()
   while (tmp->next) {
     tmp = tmp->next;
     cex.push_back(tmp->target.term);
-    assert(conc_ts_.only_curr(tmp->target.term));
+    assert(ts_.only_curr(tmp->target.term));
   }
 
   if (cex.size() == 1) {
@@ -311,7 +310,7 @@ bool IC3IA::add_predicate(const Term & pred)
     return false;
   }
 
-  assert(ts_->only_curr(pred));
+  assert(ts_.only_curr(pred));
   logger.log(2, "adding predicate {}", pred);
   predset_.insert(pred);
   // add predicate to abstraction and get the new constraint
@@ -332,7 +331,7 @@ void IC3IA::register_symbol_mappings(size_t i)
 
   UnorderedTermMap & cache = to_solver_.get_cache();
   Term unrolled_sv;
-  for (auto const&sv : ts_->statevars()) {
+  for (const auto &sv : ts_.statevars()) {
     unrolled_sv = unroller_.at_time(sv, i);
     cache[to_interpolator_.transfer_term(unrolled_sv)] = unrolled_sv;
   }
diff --git a/engines/ic3ia.h b/engines/ic3ia.h
index b7a5bb450..e972c55be 100644
--- a/engines/ic3ia.h
+++ b/engines/ic3ia.h
@@ -41,7 +41,8 @@ class IC3IA : public IC3
   // itp_se is the SolverEnum for the interpolator
 
 
-  IC3IA(Property & p, const smt::SmtSolver & s, smt::SmtSolver itp,
+  IC3IA(const Property & p, const TransitionSystem & ts,
+        const smt::SmtSolver & s, const smt::SmtSolver & itp,
         PonoOptions opt = PonoOptions());
 
   virtual ~IC3IA() {}
@@ -53,12 +54,7 @@ class IC3IA : public IC3
   //       because we will pass them to ia_ and they must be
   //       be initialized first
 
-  TransitionSystem & conc_ts_;  ///< convenient reference to the concrete ts
-
-  RelationalTransitionSystem abs_ts_;  ///< the abstract ts
-                                       ///< after initialize, ts_ will point to
-                                       ///< this because the methods from IC3
-                                       ///< should operate on the abstraction
+  TransitionSystem conc_ts_; 
 
   ImplicitPredicateAbstractor ia_;
 
diff --git a/engines/interpolantmc.cpp b/engines/interpolantmc.cpp
index 3f0ade016..1d417e6d4 100644
--- a/engines/interpolantmc.cpp
+++ b/engines/interpolantmc.cpp
@@ -26,11 +26,12 @@ using namespace smt;
 
 namespace pono {
 
-InterpolantMC::InterpolantMC(Property & p,
+InterpolantMC::InterpolantMC(const Property & p,
+                             const TransitionSystem & ts,
                              const SmtSolver & slv,
                              const SmtSolver & itp,
                              PonoOptions opt)
-    : super(p, slv, opt),
+    : super(p, ts, slv, opt),
       interpolator_(itp),
       to_interpolator_(interpolator_),
       to_solver_(solver_)
@@ -55,11 +56,11 @@ void InterpolantMC::initialize()
   // B)
   UnorderedTermMap & cache = to_solver_.get_cache();
   Term tmp1;
-  for (auto s : ts_->statevars()) {
+  for (const auto &s : ts_.statevars()) {
     tmp1 = unroller_.at_time(s, 1);
     cache[to_interpolator_.transfer_term(tmp1)] = tmp1;
   }
-  for (auto i : ts_->inputvars()) {
+  for (const auto &i : ts_.inputvars()) {
     tmp1 = unroller_.at_time(i, 1);
     cache[to_interpolator_.transfer_term(tmp1)] = tmp1;
   }
@@ -67,17 +68,17 @@ void InterpolantMC::initialize()
   // need to copy over UF as well
   UnorderedTermSet free_symbols;
   get_free_symbols(bad_, free_symbols);
-  get_free_symbols(ts_->init(), free_symbols);
-  get_free_symbols(ts_->trans(), free_symbols);
-  for (auto s : free_symbols) {
+  get_free_symbols(ts_.init(), free_symbols);
+  get_free_symbols(ts_.trans(), free_symbols);
+  for (const auto &s : free_symbols) {
     if (s->get_sort()->get_sort_kind() == FUNCTION) {
       cache[to_interpolator_.transfer_term(s)] = s;
     }
   }
 
   concrete_cex_ = false;
-  init0_ = unroller_.at_time(ts_->init(), 0);
-  transA_ = unroller_.at_time(ts_->trans(), 0);
+  init0_ = unroller_.at_time(ts_.init(), 0);
+  transA_ = unroller_.at_time(ts_.trans(), 0);
   transB_ = solver_->make_term(true);
   bad_disjuncts_ = solver_->make_term(false);
 }
@@ -180,7 +181,7 @@ bool InterpolantMC::step(int i)
   assert(i > 0);
   // extend the unrolling
   transB_ =
-      solver_->make_term(And, transB_, unroller_.at_time(ts_->trans(), i));
+      solver_->make_term(And, transB_, unroller_.at_time(ts_.trans(), i));
   ++reached_k_;
 
   return false;
diff --git a/engines/interpolantmc.h b/engines/interpolantmc.h
index bbfd0b2ff..82bb2f8ed 100644
--- a/engines/interpolantmc.h
+++ b/engines/interpolantmc.h
@@ -27,7 +27,8 @@ class InterpolantMC : public Prover
 {
  public:
   // IMPORTANT: assume the property was built using the interpolating solver
-  InterpolantMC(Property & p,
+  InterpolantMC(const Property & p,
+                const TransitionSystem & ts,
                 const smt::SmtSolver & slv,
                 const smt::SmtSolver & itp,
                 PonoOptions opt = PonoOptions());
@@ -40,7 +41,7 @@ class InterpolantMC : public Prover
 
   ProverResult check_until(int k) override;
 
- private:
+ protected:
   bool step(int i);
   bool step_0();
 
diff --git a/engines/kinduction.cpp b/engines/kinduction.cpp
index 69261be4b..3f696c170 100644
--- a/engines/kinduction.cpp
+++ b/engines/kinduction.cpp
@@ -21,9 +21,10 @@ using namespace smt;
 
 namespace pono {
 
-KInduction::KInduction(Property & p, const SmtSolver & solver,
+KInduction::KInduction(const Property & p, const TransitionSystem & ts,
+                       const SmtSolver & solver,
                        PonoOptions opt)
-  : super(p, solver, opt)
+  : super(p, ts, solver, opt)
 {
 }
 
@@ -36,12 +37,13 @@ void KInduction::initialize()
   }
 
   super::initialize();
+
   // NOTE: There's an implicit assumption that this solver is only used for
   // model checking once Otherwise there could be conflicting assertions to
   // the solver or it could just be polluted with redundant assertions in the
   // future we can use solver_->reset_assertions(), but it is not currently
   // supported in boolector
-  init0_ = unroller_.at_time(ts_->init(), 0);
+  init0_ = unroller_.at_time(ts_.init(), 0);
   false_ = solver_->make_term(false);
   simple_path_ = solver_->make_term(true);
 }
@@ -80,8 +82,9 @@ bool KInduction::base_step(int i)
   }
   solver_->pop();
 
-  solver_->assert_formula(unroller_.at_time(ts_->trans(), i));
-  solver_->assert_formula(unroller_.at_time(property_.prop(), i));
+  const Term &prop = solver_->make_term(Not, bad_);
+  solver_->assert_formula(unroller_.at_time(ts_.trans(), i));
+  solver_->assert_formula(unroller_.at_time(prop, i));
 
   return true;
 }
@@ -96,7 +99,7 @@ bool KInduction::inductive_step(int i)
   solver_->assert_formula(simple_path_);
   solver_->assert_formula(unroller_.at_time(bad_, i + 1));
 
-  if (ts_->statevars().size() && check_simple_path_lazy(i + 1)) {
+  if (ts_.statevars().size() && check_simple_path_lazy(i + 1)) {
     return true;
   }
 
@@ -109,10 +112,10 @@ bool KInduction::inductive_step(int i)
 
 Term KInduction::simple_path_constraint(int i, int j)
 {
-  assert(ts_->statevars().size());
+  assert(ts_.statevars().size());
 
   Term disj = false_;
-  for (auto v : ts_->statevars()) {
+  for (const auto &v : ts_.statevars()) {
     Term vi = unroller_.at_time(v, i);
     Term vj = unroller_.at_time(v, j);
     Term eq = solver_->make_term(PrimOp::Equal, vi, vj);
diff --git a/engines/kinduction.h b/engines/kinduction.h
index 281364406..3509c1b4a 100644
--- a/engines/kinduction.h
+++ b/engines/kinduction.h
@@ -23,7 +23,8 @@ namespace pono {
 class KInduction : public Prover
 {
  public:
-  KInduction(Property & p, const smt::SmtSolver & solver,
+  KInduction(const Property & p, const TransitionSystem & ts,
+             const smt::SmtSolver & solver,
              PonoOptions opt = PonoOptions());
 
   virtual ~KInduction();
diff --git a/engines/mbic3.cpp b/engines/mbic3.cpp
index 3a1698f27..d58f80aaa 100644
--- a/engines/mbic3.cpp
+++ b/engines/mbic3.cpp
@@ -67,22 +67,23 @@ static void split_eq(SmtSolver & solver, const TermVec & in, TermVec & out)
   }
 }
 
-ModelBasedIC3::ModelBasedIC3(Property & p, const SmtSolver & slv,
+ModelBasedIC3::ModelBasedIC3(const Property & p, const TransitionSystem & ts,
+                             const SmtSolver & slv,
                              PonoOptions opt)
-  : super(p, slv, opt)
+  : super(p, ts, slv, opt)
 {
   solver_->set_opt("produce-unsat-cores", "true");
 }
 
 IC3Formula ModelBasedIC3::get_model_ic3formula(TermVec * out_inputs,
-                                                TermVec * out_nexts) const
+                                               TermVec * out_nexts) const
 {
   DisjointSet ds(disjoint_set_rank);
   TermVec cube_lits;
-  const UnorderedTermSet & statevars = ts_->statevars();
+  const UnorderedTermSet & statevars = ts_.statevars();
 
   if (out_inputs) {
-    out_inputs->reserve(ts_->inputvars().size());
+    out_inputs->reserve(ts_.inputvars().size());
   }
   if (out_nexts) {
     out_nexts->reserve(statevars.size());
@@ -92,10 +93,10 @@ IC3Formula ModelBasedIC3::get_model_ic3formula(TermVec * out_inputs,
     Term val = solver_->get_value(v);
     cube_lits.push_back(solver_->make_term(Equal, v, val));
     ds.add(v, val);
-    assert(ts_->is_curr_var(v));
+    assert(ts_.is_curr_var(v));
 
     if (out_nexts) {
-      Term nv = ts_->next(v);
+      Term nv = ts_.next(v);
       out_nexts->push_back(
           solver_->make_term(Equal, nv, solver_->get_value(nv)));
     }
@@ -110,7 +111,7 @@ IC3Formula ModelBasedIC3::get_model_ic3formula(TermVec * out_inputs,
   }
 
   if (out_inputs) {
-    for (const auto &iv : ts_->inputvars()) {
+    for (const auto &iv : ts_.inputvars()) {
       out_inputs->push_back(
           solver_->make_term(Equal, iv, solver_->get_value(iv)));
     }
@@ -192,7 +193,7 @@ vector<IC3Formula> ModelBasedIC3::inductive_generalization(size_t i,
             for (const auto &t : tmp) {
               l = label(t);
               solver_->assert_formula(
-                  solver_->make_term(Implies, l, ts_->next(t)));
+                  solver_->make_term(Implies, l, ts_.next(t)));
               bool_assump.push_back(l);
             }
 
@@ -241,22 +242,22 @@ vector<IC3Formula> ModelBasedIC3::inductive_generalization(size_t i,
     } else if (options_.mbic3_indgen_mode == 1) {
       TermVec tmp, lits, red_lits;
       for (const auto &a : c.children) {
-        tmp.push_back(ts_->next(a));
+        tmp.push_back(ts_.next(a));
       }
       split_eq(solver_, tmp, lits);
 
       // ( (frame /\ trans /\ not(c)) \/ init') /\ c' is unsat
       Term formula = make_and({ get_frame_term(i - 1),
-                                ts_->trans(),
+                                ts_.trans(),
                                 solver_->make_term(Not, c.term) });
-      formula = solver_->make_term(Or, formula, ts_->next(ts_->init()));
+      formula = solver_->make_term(Or, formula, ts_.next(ts_.init()));
       reducer_.reduce_assump_unsatcore(formula, lits, red_lits, NULL,
                                        options_.ic3_gen_max_iter_,
                                        options_.random_seed_);
       TermVec curr_lits;
       curr_lits.reserve(red_lits.size());
       for (const auto &l : red_lits) {
-        curr_lits.push_back(ts_->curr(l));
+        curr_lits.push_back(ts_.curr(l));
       }
       gen_res.push_back(ic3formula_negate(ic3formula_conjunction(curr_lits)));
     } else if (options_.mbic3_indgen_mode == 2) {
@@ -268,15 +269,15 @@ vector<IC3Formula> ModelBasedIC3::inductive_generalization(size_t i,
 
       // ( (frame /\ trans /\ not(c)) \/ init') /\ c' is unsat
       Term formula = make_and({ get_frame_term(i - 1),
-                                ts_->trans(),
+                                ts_.trans(),
                                 solver_->make_term(Not, make_and(conjuncts)) });
-      formula = solver_->make_term(Or, formula, ts_->next(ts_->init()));
+      formula = solver_->make_term(Or, formula, ts_.next(ts_.init()));
 
       Term int_A = to_interpolator_->transfer_term(formula, BOOL);
       // still use c in B
       // only split equalities in A to encourage more general unsat proofs /
       // interpolants
-      Term int_B = to_interpolator_->transfer_term(ts_->next(c.term), BOOL);
+      Term int_B = to_interpolator_->transfer_term(ts_.next(c.term), BOOL);
 
       Term interp;
       Result r = interpolator_->get_interpolant(int_A, int_B, interp);
@@ -292,7 +293,7 @@ vector<IC3Formula> ModelBasedIC3::inductive_generalization(size_t i,
         // a single formula, {c} from the conjunctive partition of the
         // interpolant
         // --> interpolant not guaranteed to be a clause
-        gen_res.push_back(ic3formula_disjunction({ ts_->curr(c) }));
+        gen_res.push_back(ic3formula_disjunction({ ts_.curr(c) }));
       }
 
     } else {
@@ -310,7 +311,7 @@ IC3Formula ModelBasedIC3::generalize_predecessor(size_t i, const IC3Formula & c)
                                   // reducer_
   DisjointSet ds(disjoint_set_rank);
   UnorderedTermMap model;
-  const UnorderedTermSet & statevars = ts_->statevars();
+  const UnorderedTermSet & statevars = ts_.statevars();
 
   TermVec cube_lits;
   cube_lits.reserve(statevars.size());
@@ -321,12 +322,12 @@ IC3Formula ModelBasedIC3::generalize_predecessor(size_t i, const IC3Formula & c)
     Term val = solver_->get_value(v);
     cube_lits.push_back(solver_->make_term(Equal, v, val));
     ds.add(v, val);
-    assert(ts_->is_curr_var(v));
+    assert(ts_.is_curr_var(v));
     assert(model.find(v) == model.end());
     model[v] = val;
 
-    Term nv = ts_->next(v);
-    assert(ts_->is_next_var(nv));
+    Term nv = ts_.next(v);
+    assert(ts_.is_next_var(nv));
     Term next_val = solver_->get_value(nv);
     next_lits.push_back(solver_->make_term(Equal, nv, next_val));
     assert(model.find(nv) == model.end());
@@ -334,7 +335,7 @@ IC3Formula ModelBasedIC3::generalize_predecessor(size_t i, const IC3Formula & c)
   }
 
   // collect input assignments
-  const UnorderedTermSet & inputvars = ts_->inputvars();
+  const UnorderedTermSet & inputvars = ts_.inputvars();
   TermVec input_lits;
   input_lits.reserve(inputvars.size());
   for (const auto &v : inputvars) {
@@ -366,14 +367,14 @@ IC3Formula ModelBasedIC3::generalize_predecessor(size_t i, const IC3Formula & c)
 
     Term formula = make_and(input_lits);
 
-    if (ts_->is_deterministic()) {
+    if (ts_.is_deterministic()) {
       // NOTE: reducer doesn't have semantics for trans_label_
       // better to just use whole trans for now
       // Optionally in the future we could add those semantics
       // to the reducer_'s solver
-      formula = solver_->make_term(And, formula, ts_->trans());
+      formula = solver_->make_term(And, formula, ts_.trans());
       formula = solver_->make_term(
-          And, formula, solver_->make_term(Not, ts_->next(c.term)));
+          And, formula, solver_->make_term(Not, ts_.next(c.term)));
     } else {
       formula = solver_->make_term(And, formula, make_and(next_lits));
 
@@ -385,10 +386,10 @@ IC3Formula ModelBasedIC3::generalize_predecessor(size_t i, const IC3Formula & c)
       // the implication could be more efficient than iff so we want to leave it
       // that way
       Term pre_formula = get_frame_term(i - 1);
-      pre_formula = solver_->make_term(And, pre_formula, ts_->trans());
+      pre_formula = solver_->make_term(And, pre_formula, ts_.trans());
       pre_formula =
           solver_->make_term(And, pre_formula, solver_->make_term(Not, c.term));
-      pre_formula = solver_->make_term(And, pre_formula, ts_->next(c.term));
+      pre_formula = solver_->make_term(And, pre_formula, ts_.next(c.term));
 
       formula = solver_->make_term(
           And, formula, solver_->make_term(Not, pre_formula));
@@ -408,14 +409,14 @@ IC3Formula ModelBasedIC3::generalize_predecessor(size_t i, const IC3Formula & c)
     res = ic3formula_conjunction(red_cube_lits);
 
   } else if (options_.ic3_pregen_ && options_.ic3_functional_preimage_) {
-    assert(ts_->is_deterministic());
+    assert(ts_.is_deterministic());
 
     UnorderedTermMap m;
     for (const auto &v : inputvars) {
       m[v] = model.at(v);
     }
     for (const auto &v : statevars) {
-      Term nv = ts_->next(v);
+      Term nv = ts_.next(v);
       m[nv] = model.at(nv);
     }
 
@@ -430,7 +431,7 @@ IC3Formula ModelBasedIC3::generalize_predecessor(size_t i, const IC3Formula & c)
 void ModelBasedIC3::check_ts() const
 {
   // check if there are arrays or uninterpreted sorts and fail if so
-  for (const auto &vec : { ts_->statevars(), ts_->inputvars() }) {
+  for (const auto &vec : { ts_.statevars(), ts_.inputvars() }) {
     for (const auto &st : vec) {
       SortKind sk = st->get_sort()->get_sort_kind();
       if (sk == ARRAY) {
@@ -478,12 +479,12 @@ void ModelBasedIC3::initialize()
 
     UnorderedTermMap & cache = to_solver_->get_cache();
     Term ns;
-    for (const auto &s : ts_->statevars()) {
+    for (const auto &s : ts_.statevars()) {
       // common variables are next states, unless used for refinement in IC3IA
       // then will refer to current state variables after untiming
       // need to cache both
       cache[to_interpolator_->transfer_term(s)] = s;
-      ns = ts_->next(s);
+      ns = ts_.next(s);
       cache[to_interpolator_->transfer_term(ns)] = ns;
     }
 
@@ -492,8 +493,8 @@ void ModelBasedIC3::initialize()
     // NOTE need to use get_free_symbols NOT get_free_symbolic_consts
     // because the latter ignores uninterpreted functions
     UnorderedTermSet free_symbols;
-    get_free_symbols(ts_->init(), free_symbols);
-    get_free_symbols(ts_->trans(), free_symbols);
+    get_free_symbols(ts_.init(), free_symbols);
+    get_free_symbols(ts_.trans(), free_symbols);
     get_free_symbols(bad_, free_symbols);
 
     for (const auto &s : free_symbols) {
diff --git a/engines/mbic3.h b/engines/mbic3.h
index c0a5216ee..1692434d3 100644
--- a/engines/mbic3.h
+++ b/engines/mbic3.h
@@ -22,7 +22,8 @@ namespace pono {
 class ModelBasedIC3 : public IC3Base
 {
  public:
-  ModelBasedIC3(Property & p, const smt::SmtSolver & s,
+  ModelBasedIC3(const Property & p, const TransitionSystem & ts,
+                const smt::SmtSolver & s,
                 PonoOptions opt = PonoOptions());
 
   virtual ~ModelBasedIC3() {}
diff --git a/engines/msat_ic3ia.cpp b/engines/msat_ic3ia.cpp
index c29f7d3b2..d754a51cb 100644
--- a/engines/msat_ic3ia.cpp
+++ b/engines/msat_ic3ia.cpp
@@ -29,14 +29,15 @@ using namespace std;
 
 namespace pono {
 
-MsatIC3IA::MsatIC3IA(Property & p, const SmtSolver & solver, PonoOptions opt)
-    : super(p, solver, opt)
+MsatIC3IA::MsatIC3IA(const Property & p, const TransitionSystem & ts,
+                     const SmtSolver & solver, PonoOptions opt)
+  : super(p, ts, solver, opt)
 {
 }
 
 ProverResult MsatIC3IA::prove()
 {
-  super::initialize();
+  initialize();
 
   if (ts_->solver()->get_solver_enum() != MSAT) {
     throw PonoException("MsatIC3IA only supports mathsat solver.");
diff --git a/engines/msat_ic3ia.h b/engines/msat_ic3ia.h
index 4590f48ae..f2756d038 100644
--- a/engines/msat_ic3ia.h
+++ b/engines/msat_ic3ia.h
@@ -25,7 +25,8 @@ namespace pono {
 class MsatIC3IA : public Prover
 {
  public:
-  MsatIC3IA(Property & p,
+  MsatIC3IA(const Property & p,
+            const TransitionSystem & ts,
             const smt::SmtSolver & solver,
             PonoOptions opt = PonoOptions());
 
diff --git a/engines/prover.cpp b/engines/prover.cpp
index f209b2f20..2f6f19618 100644
--- a/engines/prover.cpp
+++ b/engines/prover.cpp
@@ -20,6 +20,7 @@
 #include <climits>
 #include <functional>
 
+#include "core/rts.h"
 #include "modifiers/static_coi.h"
 #include "smt/available_solvers.h"
 #include "utils/logger.h"
@@ -29,14 +30,15 @@ using namespace std;
 
 namespace pono {
 
-Prover::Prover(Property & p, const smt::SmtSolver & s, PonoOptions opt)
+Prover::Prover(const Property & p, const TransitionSystem & ts,
+               const smt::SmtSolver & s, PonoOptions opt)
     : initialized_(false),
       solver_(s),
       to_prover_solver_(s),
-      property_(p, to_prover_solver_),
-      ts_(&property_.transition_system()),
-      orig_ts_(p.transition_system()),
-      unroller_(*ts_, solver_),
+      orig_property_(p),
+      orig_ts_(ts),
+      ts_(ts, to_prover_solver_),
+      unroller_(ts_, solver_),
       options_(opt)
 {
 }
@@ -50,8 +52,19 @@ void Prover::initialize()
   }
 
   reached_k_ = -1;
-  bad_ = solver_->make_term(smt::PrimOp::Not, property_.prop());
-  assert(ts_->only_curr(bad_));
+
+  if (!bad_) {
+    // initialize bad_ if it is not set already
+    const Term &prop_term = (ts_.solver() == orig_property_.solver())
+      ? orig_property_.prop()
+      : to_prover_solver_.transfer_term(orig_property_.prop());
+    bad_ = solver_->make_term(smt::PrimOp::Not, prop_term);
+    assert(ts_.only_curr(bad_));
+  }
+
+  if (!ts_.only_curr(bad_)) {
+    throw PonoException("Property should not contain inputs or next state variables");
+  }
 
   initialized_ = true;
 }
@@ -85,10 +98,10 @@ bool Prover::witness(std::vector<UnorderedTermMap> & out)
           "currently incompatible with witness generation.");
     // need to add symbols to cache
     UnorderedTermMap & cache = to_orig_ts_solver.get_cache();
-    for (auto v : orig_ts_.statevars()) {
+    for (const auto &v : orig_ts_.statevars()) {
       cache[to_prover_solver_.transfer_term(v)] = v;
     }
-    for (auto v : orig_ts_.inputvars()) {
+    for (const auto &v : orig_ts_.inputvars()) {
       cache[to_prover_solver_.transfer_term(v)] = v;
     }
 
@@ -109,15 +122,15 @@ bool Prover::witness(std::vector<UnorderedTermMap> & out)
     out.push_back(UnorderedTermMap());
     UnorderedTermMap & map = out.back();
 
-    for (auto v : orig_ts_.statevars()) {
-      SortKind sk = v->get_sort()->get_sort_kind();
-      Term pv = transfer_to_prover_as(v, sk);
+    for (const auto &v : orig_ts_.statevars()) {
+      const SortKind &sk = v->get_sort()->get_sort_kind();
+      const Term &pv = transfer_to_prover_as(v, sk);
       map[v] = transfer_to_orig_ts_as(wit_map.at(pv), sk);
     }
 
-    for (auto v : orig_ts_.inputvars()) {
-      SortKind sk = v->get_sort()->get_sort_kind();
-      Term pv = transfer_to_prover_as(v, sk);
+    for (const auto &v : orig_ts_.inputvars()) {
+      const SortKind &sk = v->get_sort()->get_sort_kind();
+      const Term &pv = transfer_to_prover_as(v, sk);
       try {
         map[v] = transfer_to_orig_ts_as(wit_map.at(pv), sk);
       }
@@ -128,9 +141,9 @@ bool Prover::witness(std::vector<UnorderedTermMap> & out)
     }
 
     if (success) {
-      for (auto elem : orig_ts_.named_terms()) {
-        SortKind sk = elem.second->get_sort()->get_sort_kind();
-        Term pt = transfer_to_prover_as(elem.second, sk);
+      for (const auto &elem : orig_ts_.named_terms()) {
+        const SortKind &sk = elem.second->get_sort()->get_sort_kind();
+        const Term &pt = transfer_to_prover_as(elem.second, sk);
         try {
           map[elem.second] = transfer_to_orig_ts_as(wit_map.at(pt), sk);
         }
@@ -170,12 +183,12 @@ Term Prover::to_orig_ts(Term t, SortKind sk)
     // need to add symbols to cache
     TermTranslator to_orig_ts_solver(orig_ts_.solver());
     UnorderedTermMap & cache = to_orig_ts_solver.get_cache();
-    for (auto v : orig_ts_.statevars()) {
+    for (const auto &v : orig_ts_.statevars()) {
       cache[to_prover_solver_.transfer_term(v)] = v;
-      Term nv = orig_ts_.next(v);
+      const Term &nv = orig_ts_.next(v);
       cache[to_prover_solver_.transfer_term(nv)] = v;
     }
-    for (auto v : orig_ts_.inputvars()) {
+    for (const auto &v : orig_ts_.inputvars()) {
       cache[to_prover_solver_.transfer_term(v)] = v;
     }
     return to_orig_ts_solver.transfer_term(t, sk);
@@ -195,20 +208,20 @@ bool Prover::compute_witness()
     witness_.push_back(UnorderedTermMap());
     UnorderedTermMap & map = witness_.back();
 
-    for (auto v : ts_->statevars()) {
-      Term vi = unroller_.at_time(v, i);
-      Term r = solver_->get_value(vi);
+    for (const auto &v : ts_.statevars()) {
+      const Term &vi = unroller_.at_time(v, i);
+      const Term &r = solver_->get_value(vi);
       map[v] = r;
     }
 
-    for (auto v : ts_->inputvars()) {
-      Term vi = unroller_.at_time(v, i);
-      Term r = solver_->get_value(vi);
+    for (const auto &v : ts_.inputvars()) {
+      const Term &vi = unroller_.at_time(v, i);
+      const Term &r = solver_->get_value(vi);
       map[v] = r;
     }
 
-    for (auto elem : ts_->named_terms()) {
-      Term ti = unroller_.at_time(elem.second, i);
+    for (const auto &elem : ts_.named_terms()) {
+      const Term &ti = unroller_.at_time(elem.second, i);
       map[elem.second] = solver_->get_value(ti);
     }
   }
diff --git a/engines/prover.h b/engines/prover.h
index af782bf04..c686cd866 100644
--- a/engines/prover.h
+++ b/engines/prover.h
@@ -39,7 +39,8 @@ enum RefineResult
 class Prover
 {
  public:
-  Prover(Property & p, const smt::SmtSolver & s,
+  Prover(const Property & p, const TransitionSystem & ts,
+         const smt::SmtSolver & s,
          PonoOptions opt = PonoOptions());
 
   virtual ~Prover();
@@ -89,25 +90,18 @@ class Prover
 
   smt::SmtSolver solver_;
   smt::TermTranslator to_prover_solver_;
-  Property property_;
-  TransitionSystem *
-      ts_;  ///< pointer to main transition system
-            ///< by default this is the one in property_
-            ///< however, this can change depending on the engine
-            ///< for example, a CEGAR technique will usually
-            ///< set the main ts_ to be the abstraction, and
-            ///< and keep a reference to the concrete transition system
-            ///< Additionally, the pointed-to transition system is NOT
-            ///< guaranteed to be fully initialized in the constructor
-            ///< of the engine
-            ///< this is because abstraction might not happen until later
-  const TransitionSystem &
-      orig_ts_;  ///< reference to original TS before copied to new solver
+
+  Property orig_property_; ///< original property before copied to new solver
+  TransitionSystem orig_ts_;  ///< original TS before copied to new solver
+
+  TransitionSystem ts_;
 
   Unroller unroller_;
 
   int reached_k_;
 
+  //TODO: add engine enum
+
   smt::Term bad_;
 
   PonoOptions options_;
diff --git a/modifiers/mod_init_prop.h b/modifiers/mod_init_prop.h
index 6359b0ed5..637cebaf3 100644
--- a/modifiers/mod_init_prop.h
+++ b/modifiers/mod_init_prop.h
@@ -2,7 +2,7 @@
 /*! \file mod_init_prop.h
 ** \verbatim
 ** Top contributors (to current version):
-**   Makai Mann
+**   Makai Mann, Ahmed Irfan
 ** This file is part of the pono project.
 ** Copyright (c) 2019 by the authors listed in the file AUTHORS
 ** in the top-level source directory) and their institutional affiliations.
@@ -14,36 +14,36 @@
 **
 **/
 
+#pragma once
+
 #include "core/ts.h"
 #include "smt-switch/utils.h"
 #include "utils/logger.h"
 #include "utils/term_analysis.h"
 
-using namespace std;
-using namespace smt;
-
 namespace pono {
 
-Term modify_init_and_prop(TransitionSystem & ts, const Term & prop)
+smt::Term modify_init_and_prop(TransitionSystem & ts, const smt::Term & prop)
 {
   logger.log(1, "Modifying init and prop");
 
   // copy constraints from before we start modifying the system
-  TermVec constraints = ts.constraints();
+  smt::TermVec constraints = ts.constraints();
 
   // replace prop if it's not already a literal
-  Sort boolsort = ts.make_sort(BOOL);
-  Term new_prop = prop;
+  smt::Sort boolsort = ts.make_sort(smt::BOOL);
+  smt::Term new_prop = prop;
   if (!is_lit(prop, boolsort)) {
     new_prop = ts.make_statevar("__propvar", boolsort);
     ts.assign_next(new_prop, prop);
   }
 
   // replace initial states
-  Term initstate1 = ts.make_statevar("__initstate1", ts.make_sort(BOOL));
+  smt::Term initstate1 = ts.make_statevar("__initstate1",
+                                          ts.make_sort(smt::BOOL));
 
-  Term init = ts.init();
-  TermVec init_constraints;
+  smt::Term init = ts.init();
+  smt::TermVec init_constraints;
   conjunctive_partition(init, init_constraints, true);
 
   ts.set_init(initstate1);
@@ -53,7 +53,7 @@ Term modify_init_and_prop(TransitionSystem & ts, const Term & prop)
     // TODO possibly refactor constraints so next state versions aren't
     // automatically added
     if (ts.no_next(c)) {
-      ts.add_constraint(ts.make_term(Implies, initstate1, c), false);
+      ts.add_constraint(ts.make_term(smt::Implies, initstate1, c), false);
     }
   }
 
@@ -62,7 +62,7 @@ Term modify_init_and_prop(TransitionSystem & ts, const Term & prop)
 
   // add initial state constraints for initstate1
   for (const auto & ic : init_constraints) {
-    ts.add_constraint(ts.make_term(Implies, initstate1, ic), false);
+    ts.add_constraint(ts.make_term(smt::Implies, initstate1, ic), false);
   }
 
   return new_prop;
diff --git a/modifiers/prop_monitor.h b/modifiers/prop_monitor.h
new file mode 100644
index 000000000..de0511b06
--- /dev/null
+++ b/modifiers/prop_monitor.h
@@ -0,0 +1,60 @@
+/*********************                                                  */
+/*! \file prop_monitor.h
+** \verbatim
+** Top contributors (to current version):
+**   Makai Mann, Ahmed Irfan
+** This file is part of the pono project.
+** Copyright (c) 2019 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file LICENSE in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief Adds a monitor for the property term and also replaces the property
+**
+**
+**/
+
+#pragma once
+
+#include "core/ts.h"
+#include "utils/logger.h"
+
+namespace pono {
+
+smt::Term add_prop_monitor(TransitionSystem & ts, const smt::Term & prop)
+{
+  logger.log(1, "Adding a monitor for the property");
+
+  smt::Term monitor;
+  size_t id = 0;
+  while (true) {
+    try {
+      monitor = ts.make_statevar("_monitor_" + std::to_string(id),
+                                 ts.make_sort(smt::BOOL));
+      break;
+    }
+    catch (SmtException & e) {
+      ++id;
+    }
+  }
+  assert(monitor);
+
+  // monitor starts true
+  ts.constrain_init(monitor);
+
+  if (ts.no_next(prop)) {
+    ts.assign_next(monitor, prop);
+  } else if (!ts.is_functional()) {
+    RelationalTransitionSystem & rts =
+      static_cast<RelationalTransitionSystem &>(ts);
+    rts.constrain_trans(rts.make_term(smt::Equal, rts.next(monitor), prop));
+  } else {
+    assert(ts.is_functional());
+    throw PonoException(
+        "Cannot use next in property of a functional transition system.");
+  }
+
+  return monitor;
+}
+
+}  // namespace pono
diff --git a/pono.cpp b/pono.cpp
index ed96fce25..66a54f7e3 100644
--- a/pono.cpp
+++ b/pono.cpp
@@ -33,6 +33,7 @@
 #include "frontends/smv_encoder.h"
 #include "modifiers/control_signals.h"
 #include "modifiers/mod_init_prop.h"
+#include "modifiers/prop_monitor.h"
 #include "modifiers/static_coi.h"
 #include "options/options.h"
 #include "printers/btor2_witness_printer.h"
@@ -52,14 +53,15 @@ using namespace std;
 
 ProverResult check_prop(PonoOptions pono_options,
                         Property & p,
-                        SmtSolver & s,
-                        SmtSolver & second_solver,
+                        const TransitionSystem & ts,
+                        const SmtSolver & s,
+                        const SmtSolver & second_solver,
                         std::vector<UnorderedTermMap> & cex)
 {
   logger.log(1, "Solving property: {}", p.name());
 
-  logger.log(3, "INIT:\n{}", p.transition_system().init());
-  logger.log(3, "TRANS:\n{}", p.transition_system().trans());
+  logger.log(3, "INIT:\n{}", ts.init());
+  logger.log(3, "TRANS:\n{}", ts.trans());
 
   Engine eng = pono_options.engine_;
 
@@ -67,13 +69,13 @@ ProverResult check_prop(PonoOptions pono_options,
   if (pono_options.ceg_prophecy_arrays_) {
     // don't instantiate the sub-prover directly
     // just pass the engine to CegProphecyArrays
-    prover = std::make_shared<CegProphecyArrays>(p, eng, s, pono_options);
+    prover = std::make_shared<CegProphecyArrays>(p, ts, eng, s, pono_options);
   } else if (eng != INTERP) {
     assert(!second_solver);
-    prover = make_prover(eng, p, s, pono_options);
+    prover = make_prover(eng, p, ts, s, pono_options);
   } else {
     assert(second_solver);
-    prover = make_prover(eng, p, s, second_solver, pono_options);
+    prover = make_prover(eng, p, ts, s, second_solver, pono_options);
   }
   assert(prover);
 
@@ -102,7 +104,7 @@ ProverResult check_prop(PonoOptions pono_options,
   } else if (r == TRUE && pono_options.check_invar_) {
     try {
       Term invar = prover->invar();
-      bool invar_passes = check_invar(p.transition_system(), p.prop(), invar);
+      bool invar_passes = check_invar(ts, p.prop(), invar);
       std::cout << "Invariant Check " << (invar_passes ? "PASSED" : "FAILED")
                 << std::endl;
       if (!invar_passes) {
@@ -252,7 +254,11 @@ int main(int argc, char ** argv)
             + " is greater than the number of properties in file "
             + pono_options.filename_ + " (" + to_string(num_props) + ")");
       }
+
       Term prop = propvec[pono_options.prop_idx_];
+      // get property name before it is rewritten
+      const string prop_name = fts.get_name(prop);
+
       if (!pono_options.clock_name_.empty()) {
         Term clock_symbol = fts.lookup(pono_options.clock_name_);
         toggle_clock(fts, clock_symbol);
@@ -287,9 +293,15 @@ int main(int argc, char ** argv)
         StaticConeOfInfluence coi(fts, { prop }, pono_options.verbosity_);
       }
 
+      if (!fts.only_curr(prop)) {
+        logger.log(1, "Got next state or input variables in property. "
+                   "Generating a monitor state.");
+        prop = add_prop_monitor(fts, prop);
+      }
+
       vector<UnorderedTermMap> cex;
-      Property p(fts, prop);
-      res = check_prop(pono_options, p, s, second_solver, cex);
+      Property p(s, prop, prop_name);
+      res = check_prop(pono_options, p, fts, s, second_solver, cex);
       // we assume that a prover never returns 'ERROR'
       assert(res != ERROR);
 
@@ -326,7 +338,11 @@ int main(int argc, char ** argv)
             + " is greater than the number of properties in file "
             + pono_options.filename_ + " (" + to_string(num_props) + ")");
       }
+
       Term prop = propvec[pono_options.prop_idx_];
+      // get property name before it is rewritten
+      const string prop_name = rts.get_name(prop);
+
       if (!pono_options.clock_name_.empty()) {
         Term clock_symbol = rts.lookup(pono_options.clock_name_);
         toggle_clock(rts, clock_symbol);
@@ -353,9 +369,15 @@ int main(int argc, char ** argv)
         StaticConeOfInfluence coi(rts, { prop }, pono_options.verbosity_);
       }
 
-      Property p(rts, prop);
+      if (!rts.only_curr(prop)) {
+        logger.log(1, "Got next state or input variables in property. "
+                   "Generating a monitor state.");
+        prop = add_prop_monitor(rts, prop);
+      }
+
+      Property p(s, prop, prop_name);
       std::vector<UnorderedTermMap> cex;
-      res = check_prop(pono_options, p, s, second_solver, cex);
+      res = check_prop(pono_options, p, rts, s, second_solver, cex);
       // we assume that a prover never returns 'ERROR'
       assert(res != ERROR);
 
diff --git a/python/pono_imp.pxd b/python/pono_imp.pxd
index 2f97eb340..d76e47ebe 100644
--- a/python/pono_imp.pxd
+++ b/python/pono_imp.pxd
@@ -68,10 +68,10 @@ cdef extern from "core/fts.h" namespace "pono":
 
 cdef extern from "core/prop.h" namespace "pono":
     cdef cppclass Property:
-        Property(const TransitionSystem& ts, c_Term p) except +
+        Property(const c_SmtSolver& ts, c_Term p) except +
         const c_Term prop() except +
-        const TransitionSystem & transition_system() except +
-
+        const c_SmtSolver & solver() except +
+        string name()
 
 cdef extern from "core/unroller.h" namespace "pono":
     cdef cppclass Unroller:
@@ -92,7 +92,8 @@ cdef extern from "core/proverresult.h" namespace "pono":
 
 cdef extern from "engines/prover.h" namespace "pono":
     cdef cppclass Prover:
-        Prover(const Property & p, c_SmtSolver & s) except +
+        Prover(const Property & p, const TransitionSystem & ts,
+               c_SmtSolver & s) except +
         void initialize() except +
         ProverResult check_until(int k) except +
         bint witness(vector[c_UnorderedTermMap] & out) except +
@@ -101,44 +102,52 @@ cdef extern from "engines/prover.h" namespace "pono":
 
 cdef extern from "engines/bmc.h" namespace "pono":
     cdef cppclass Bmc(Prover):
-        Bmc(const Property & p, c_SmtSolver & solver) except +
+        Bmc(const Property & p, const TransitionSystem & ts,
+            c_SmtSolver & solver) except +
 
 
 cdef extern from "engines/kinduction.h" namespace "pono":
     cdef cppclass KInduction(Prover):
-        KInduction(const Property & p, c_SmtSolver & solver) except +
+        KInduction(const Property & p, const TransitionSystem & ts,
+                   c_SmtSolver & solver) except +
 
 
 cdef extern from "engines/bmc_simplepath.h" namespace "pono":
     cdef cppclass BmcSimplePath(KInduction):
-        BmcSimplePath(const Property & p, c_SmtSolver & solver) except +
+        BmcSimplePath(const Property & p, const TransitionSystem & ts,
+                      c_SmtSolver & solver) except +
 
 
 cdef extern from "engines/ic3.h" namespace "pono":
     cdef cppclass IC3(Prover):
-        IC3(const Property & p, c_SmtSolver & solver) except +
+        IC3(const Property & p, const TransitionSystem & ts,
+            c_SmtSolver & solver) except +
 
 
 cdef extern from "engines/ic3ia.h" namespace "pono":
     cdef cppclass IC3IA(Prover):
-        IC3IA(const Property & p, c_SmtSolver & solver, c_SmtSolver & interpolator) except +
+        IC3IA(const Property & p, const TransitionSystem & ts,
+              c_SmtSolver & solver, c_SmtSolver & interpolator) except +
 
 
 cdef extern from "engines/interpolantmc.h" namespace "pono":
     cdef cppclass InterpolantMC(Prover):
-        InterpolantMC(const Property & p, c_SmtSolver & s, c_SmtSolver & interpolator) except +
+        InterpolantMC(const Property & p, const TransitionSystem & ts,
+                      c_SmtSolver & s, c_SmtSolver & interpolator) except +
 
 
 cdef extern from "engines/mbic3.h" namespace "pono":
     cdef cppclass ModelBasedIC3(Prover):
-        ModelBasedIC3(const Property & p, c_SmtSolver & solver) except +
+        ModelBasedIC3(const Property & p, const TransitionSystem & ts,
+                      c_SmtSolver & solver) except +
 
 
 # WITH_MSAT_IC3IA is set in python/CMakeLists.txt via the --compile-time-env flag of Cython
 IF WITH_MSAT_IC3IA == "ON":
     cdef extern from "engines/msat_ic3ia.h" namespace "pono":
         cdef cppclass MsatIC3IA(Prover):
-            MsatIC3IA(const Property & p, c_SmtSolver & s) except +
+            MsatIC3IA(const Property & p, const TransitionSystem & ts,
+                      c_SmtSolver & s) except +
 
 
 cdef extern from "frontends/btor2_encoder.h" namespace "pono":
@@ -164,6 +173,9 @@ cdef extern from "modifiers/static_coi.h" namespace "pono":
                         const c_TermVec & to_keep,
                         int verbosity) except +
 
+cdef extern from "modifiers/prop_monitor.h" namespace "pono":
+    c_Term add_prop_monitor(TransitionSystem & ts,
+                            const c_Term & prop) except +
 
 cdef extern from "modifiers/history_modifier.h" namespace "pono":
     cdef cppclass HistoryModifier:
diff --git a/python/pono_imp.pxi b/python/pono_imp.pxi
index 23d0b9708..2893d5b87 100644
--- a/python/pono_imp.pxi
+++ b/python/pono_imp.pxi
@@ -30,6 +30,7 @@ IF WITH_COREIR == "ON":
     from pono_imp cimport CoreIREncoder as c_CoreIREncoder
 from pono_imp cimport HistoryModifier as c_HistoryModifier
 from pono_imp cimport StaticConeOfInfluence as c_StaticConeOfInfluence
+from pono_imp cimport add_prop_monitor as c_add_prop_monitor
 from pono_imp cimport VCDWitnessPrinter as c_VCDWitnessPrinter
 from pono_imp cimport set_global_logger_verbosity as c_set_global_logger_verbosity
 
@@ -350,23 +351,23 @@ cdef class FunctionalTransitionSystem(__AbstractTransitionSystem):
 
 cdef class Property:
     cdef c_Property* cp
-    cdef __AbstractTransitionSystem ts
-    def __cinit__(self, __AbstractTransitionSystem ts, Term p):
-        self.cp = new c_Property(ts.cts[0], p.ct)
-        self.ts = ts
+    cdef SmtSolver _solver
+    def __cinit__(self, SmtSolver s, Term p):
+        self.cp = new c_Property(s.css, p.ct)
+        self._solver = s
 
     def __dealloc__(self):
         del self.cp
 
     @property
     def prop(self):
-        cdef Term p = Term(self.ts.solver)
+        cdef Term p = Term(self._solver)
         p.ct = dref(self.cp).prop()
         return p
 
     @property
-    def transition_system(self):
-        return self.ts
+    def solver(self):
+        return self._solver
 
 
 cdef class Unroller:
@@ -397,6 +398,7 @@ cdef class __AbstractProver:
     # this pointer is allocated and deallocated by derived classes
     cdef c_Prover* cp
     cdef Property _property
+    cdef __AbstractTransitionSystem _ts
     cdef SmtSolver _solver
 
     def initialize(self):
@@ -455,8 +457,9 @@ cdef class __AbstractProver:
 
 
 cdef class Bmc(__AbstractProver):
-    def __cinit__(self, Property p, SmtSolver s):
-        self.cp = new c_Bmc(p.cp[0], s.css)
+    def __cinit__(self, Property p, __AbstractTransitionSystem ts, SmtSolver s):
+        self.cp = new c_Bmc(p.cp[0], ts.cts[0], s.css)
+        self._ts = ts
         self._solver = s
 
     def __dealloc__(self):
@@ -464,8 +467,9 @@ cdef class Bmc(__AbstractProver):
 
 
 cdef class KInduction(__AbstractProver):
-    def __cinit__(self, Property p, SmtSolver s):
-        self.cp = new c_KInduction(p.cp[0], s.css)
+    def __cinit__(self, Property p, __AbstractTransitionSystem ts, SmtSolver s):
+        self.cp = new c_KInduction(p.cp[0], ts.cts[0], s.css)
+        self._ts = ts
         self._solver = s
 
     def __dealloc__(self):
@@ -473,8 +477,9 @@ cdef class KInduction(__AbstractProver):
 
 
 cdef class BmcSimplePath(__AbstractProver):
-    def __cinit__(self, Property p, SmtSolver s):
-        self.cp = new c_BmcSimplePath(p.cp[0], s.css)
+    def __cinit__(self, Property p, __AbstractTransitionSystem ts, SmtSolver s):
+        self.cp = new c_BmcSimplePath(p.cp[0], ts.cts[0], s.css)
+        self._ts = ts
         self._solver = s
 
     def __dealloc__(self):
@@ -485,8 +490,8 @@ cdef class IC3(__AbstractProver):
     '''
     Bit-level IC3 variant
     '''
-    def __cinit__(self, Property p, SmtSolver s):
-        self.cp = new c_IC3(p.cp[0], s.css)
+    def __cinit__(self, Property p, __AbstractTransitionSystem ts, SmtSolver s):
+        self.cp = new c_IC3(p.cp[0], ts.cts[0], s.css)
         self._solver = s
 
     def __dealloc__(self):
@@ -497,8 +502,9 @@ cdef class IC3IA(__AbstractProver):
     '''
     IC3 via Implicit Predicate Abstraction
     '''
-    def __cinit__(self, Property p, SmtSolver s, SmtSolver interp):
-        self.cp = new c_IC3IA(p.cp[0], s.css, interp.css)
+    def __cinit__(self, Property p, __AbstractTransitionSystem ts, SmtSolver s, SmtSolver interp):
+        self.cp = new c_IC3IA(p.cp[0], ts.cts[0], s.css, interp.css)
+        self._ts = ts
         self._solver = s
 
     def __dealloc__(self):
@@ -506,8 +512,9 @@ cdef class IC3IA(__AbstractProver):
 
 
 cdef class InterpolantMC(__AbstractProver):
-    def __cinit__(self, Property p, SmtSolver s, SmtSolver interp):
-        self.cp = new c_InterpolantMC(p.cp[0], s.css, interp.css)
+    def __cinit__(self, Property p, __AbstractTransitionSystem ts, SmtSolver s, SmtSolver interp):
+        self.cp = new c_InterpolantMC(p.cp[0], ts.cts[0], s.css, interp.css)
+        self._ts = ts
         self._solver = s
 
     def __dealloc__(self):
@@ -515,8 +522,9 @@ cdef class InterpolantMC(__AbstractProver):
 
 
 cdef class ModelBasedIC3(__AbstractProver):
-    def __cinit__(self, Property p, SmtSolver s):
-        self.cp = new c_ModelBasedIC3(p.cp[0], s.css)
+    def __cinit__(self, Property p, __AbstractTransitionSystem ts, SmtSolver s):
+        self.cp = new c_ModelBasedIC3(p.cp[0], ts.cts[0], s.css)
+        self._ts = ts
         self._solver = s
 
     def __dealloc__(self):
@@ -525,8 +533,9 @@ cdef class ModelBasedIC3(__AbstractProver):
 
 IF WITH_MSAT_IC3IA == "ON":
     cdef class MsatIC3IA(__AbstractProver):
-        def __cinit__(self, Property p, SmtSolver s):
-            self.cp = new c_MsatIC3IA(p.cp[0], s.css)
+        def __cinit__(self, Property p, __AbstractTransitionSystem ts, SmtSolver s):
+            self.cp = new c_MsatIC3IA(p.cp[0], ts.cts[0], s.css)
+            self._ts = ts
             self._solver = s
 
         def __dealloc__(self):
@@ -557,6 +566,9 @@ IF WITH_COREIR == "ON":
         def __dealloc__(self):
             del self.cbe
 
+def add_prop_monitor(__AbstractTransitionSystem ts, Term prop):
+    c_add_prop_monitor(dref(ts.cts), prop.ct)
+
 cdef class HistoryModifier:
     cdef c_HistoryModifier * chm
     cdef __AbstractTransitionSystem _ts
diff --git a/utils/make_provers.cpp b/utils/make_provers.cpp
index b2cb4d000..eb61b6269 100644
--- a/utils/make_provers.cpp
+++ b/utils/make_provers.cpp
@@ -36,37 +36,38 @@ namespace pono {
 vector<Engine> all_engines() { return { BMC, BMC_SP, KIND, INTERP, MBIC3 }; }
 
 shared_ptr<Prover> make_prover(Engine e,
-                               Property & p,
-                               SmtSolver & slv,
+                               const Property & p,
+                               const TransitionSystem & ts,
+                               const SmtSolver & slv,
                                PonoOptions opts)
 {
   if (e == BMC) {
-    return make_shared<Bmc>(p, slv, opts);
+    return make_shared<Bmc>(p, ts, slv, opts);
   } else if (e == BMC_SP) {
-    return make_shared<BmcSimplePath>(p, slv, opts);
+    return make_shared<BmcSimplePath>(p, ts, slv, opts);
   } else if (e == KIND) {
-    return make_shared<KInduction>(p, slv, opts);
+    return make_shared<KInduction>(p, ts, slv, opts);
   } else if (e == INTERP) {
 #ifdef WITH_MSAT
     SmtSolver s = create_interpolating_solver(SolverEnum::MSAT_INTERPOLATOR);
-    return make_prover(e, p, slv, s, opts);
+    return make_prover(e, p, ts, slv, s, opts);
 #else
     throw PonoException(
         "Interpolant-based modelchecking requires an interpolator");
 #endif
   } else if (e == MBIC3) {
-    return make_shared<ModelBasedIC3>(p, slv, opts);
+    return make_shared<ModelBasedIC3>(p, ts, slv, opts);
   } else if (e == IC3IA_ENGINE) {
 #ifdef WITH_MSAT
     SmtSolver s = create_interpolating_solver(SolverEnum::MSAT_INTERPOLATOR);
-    return make_prover(e, p, slv, s, opts);
+    return make_prover(e, p, ts, slv, s, opts);
 #else
     throw PonoException(
         "IC3IA uses MathSAT for interpolants, but not built with MathSAT");
 #endif
 #ifdef WITH_MSAT_IC3IA
   } else if (e == MSAT_IC3IA) {
-    return make_shared<MsatIC3IA>(p, slv, opts);
+    return make_shared<MsatIC3IA>(p, ts, slv, opts);
 #endif
   } else {
     throw PonoException("Unhandled engine");
@@ -74,15 +75,16 @@ shared_ptr<Prover> make_prover(Engine e,
 }
 
 shared_ptr<Prover> make_prover(Engine e,
-                               Property & p,
-                               SmtSolver & slv,
-                               SmtSolver & itp,
+                               const Property & p,
+                               const TransitionSystem & ts,
+                               const SmtSolver & slv,
+                               const SmtSolver & itp,
                                PonoOptions opts)
 {
   if (e == INTERP) {
-    return make_shared<InterpolantMC>(p, slv, itp, opts);
+    return make_shared<InterpolantMC>(p, ts, slv, itp, opts);
   } else if (e == IC3IA_ENGINE) {
-    return make_shared<IC3IA>(p, slv, itp, opts);
+    return make_shared<IC3IA>(p, ts, slv, itp, opts);
   } else {
     throw PonoException(
         "Got unexpected engine when passing a solver and interpolator to "
diff --git a/utils/make_provers.h b/utils/make_provers.h
index 2340f0519..53847303a 100644
--- a/utils/make_provers.h
+++ b/utils/make_provers.h
@@ -23,13 +23,15 @@ namespace pono {
 std::vector<Engine> all_engines();
 
 std::shared_ptr<Prover> make_prover(Engine e,
-                                    Property & p,
-                                    smt::SmtSolver & slv,
+                                    const Property & p,
+                                    const TransitionSystem & ts,
+                                    const smt::SmtSolver & slv,
                                     PonoOptions opts = PonoOptions());
 
 std::shared_ptr<Prover> make_prover(Engine e,
-                                    Property & p,
-                                    smt::SmtSolver & slv,
-                                    smt::SmtSolver & itp,
+                                    const Property & p,
+                                    const TransitionSystem & ts,
+                                    const smt::SmtSolver & slv,
+                                    const smt::SmtSolver & itp,
                                     PonoOptions opts = PonoOptions());
 }  // namespace pono


Test patch:
diff --git a/tests/encoders/test_btor2.cpp b/tests/encoders/test_btor2.cpp
index 012b9c560..e09bbb3bc 100644
--- a/tests/encoders/test_btor2.cpp
+++ b/tests/encoders/test_btor2.cpp
@@ -48,8 +48,8 @@ TEST_P(Btor2UnitTests, OverflowEncoding)
   filename += "/tests/encoders/inputs/btor2/mulo-test.btor2";
   BTOR2Encoder be(filename, fts);
   EXPECT_EQ(be.propvec().size(), 1);
-  Property p(fts, be.propvec()[0]);
-  KInduction kind(p, s);
+  Property p(fts.solver(), be.propvec()[0]);
+  KInduction kind(p, fts, s);
   ProverResult r = kind.check_until(2);
   EXPECT_EQ(r, ProverResult::TRUE);
 }
diff --git a/tests/encoders/test_smv.cpp b/tests/encoders/test_smv.cpp
index 0d89fa246..76057991a 100644
--- a/tests/encoders/test_smv.cpp
+++ b/tests/encoders/test_smv.cpp
@@ -36,8 +36,8 @@ TEST_P(SmvFileUnitTests, Encode)
   cout << "Reading file: " << filename << endl;
   SMVEncoder se(filename, rts);
 
-  Property prop(rts, se.propvec()[0]);
-  KInduction kind(prop, s);
+  Property prop(rts.solver(), se.propvec()[0]);
+  KInduction kind(prop, rts, s);
   ProverResult res = kind.check_until(10);
   EXPECT_EQ(res, benchmark.second);
 }
diff --git a/tests/python/test_engines.py b/tests/python/test_engines.py
index 301354f24..58aa4fd07 100644
--- a/tests/python/test_engines.py
+++ b/tests/python/test_engines.py
@@ -5,7 +5,9 @@
 import pono
 import available_solvers
 
-def build_simple_alu_fts(s:ss.SmtSolver)->pono.Property:
+from typing import Tuple
+
+def build_simple_alu_fts(s:ss.SmtSolver)->Tuple[pono.Property, pono.FunctionalTransitionSystem]:
     '''
     Creates a simple alu transition system
     @param s - an SmtSolver from smt_switch
@@ -46,19 +48,17 @@ def build_simple_alu_fts(s:ss.SmtSolver)->pono.Property:
                                      s.make_term(BVSub, a, b)))
 
     # Create a property: (spec_cnt == imp_cnt - 1)
-    prop = pono.Property(fts, s.make_term(Equal,
-                                       spec_res,
-                                       imp_res))
-    return prop
+    prop = pono.Property(s, s.make_term(Equal, spec_res, imp_res))
+    return prop, fts
 
 @pytest.mark.parametrize("create_solver", ss.solvers.values())
 def test_bmc(create_solver):
     s = create_solver(False)
     s.set_opt('produce-models', 'true')
     s.set_opt('incremental', 'true')
-    prop = build_simple_alu_fts(s)
+    prop, ts = build_simple_alu_fts(s)
 
-    bmc = pono.Bmc(prop, s)
+    bmc = pono.Bmc(prop, ts, s)
     res = bmc.check_until(10)
 
     assert res is None, "BMC shouldn't be able to solve"
@@ -68,9 +68,9 @@ def test_kind(create_solver):
     s = create_solver(False)
     s.set_opt('produce-models', 'true')
     s.set_opt('incremental', 'true')
-    prop = build_simple_alu_fts(s)
+    prop, ts = build_simple_alu_fts(s)
 
-    kind = pono.KInduction(prop, s)
+    kind = pono.KInduction(prop, ts, s)
     res = kind.check_until(10)
 
     assert res is None, "KInduction shouldn't be able to solve this property"
@@ -83,9 +83,9 @@ def test_interp(solver_and_interpolator):
     s.set_opt('incremental', 'true')
     itp = solver_and_interpolator[1]()
 
-    prop = build_simple_alu_fts(s)
+    prop, ts = build_simple_alu_fts(s)
 
-    ic3ia = pono.IC3IA(prop, s, itp)
+    ic3ia = pono.IC3IA(prop, ts, s, itp)
     res = ic3ia.check_until(10)
 
     assert res is True, "IC3IA be able to solve this property"
@@ -98,9 +98,9 @@ def test_interp(solver_and_interpolator):
     s.set_opt('incremental', 'true')
     itp = solver_and_interpolator[1]()
 
-    prop = build_simple_alu_fts(s)
+    prop, ts = build_simple_alu_fts(s)
 
-    interp = pono.InterpolantMC(prop, s, itp)
+    interp = pono.InterpolantMC(prop, ts, s, itp)
     res = interp.check_until(10)
 
     assert res is True, "InterpolantMC be able to solve this property"
@@ -110,16 +110,16 @@ def test_kind_inductive_prop(create_solver):
     s = create_solver(False)
     s.set_opt('produce-models', 'true')
     s.set_opt('incremental', 'true')
-    prop = build_simple_alu_fts(s)
+    prop, ts = build_simple_alu_fts(s)
 
-    states = {str(sv):sv for sv in prop.transition_system.statevars}
+    states = {str(sv):sv for sv in ts.statevars}
 
-    prop = pono.Property(prop.transition_system,
-                      s.make_term(And,
-                                  s.make_term(Equal, states['cfg'], s.make_term(0, s.make_sort(BV, 1))),
-                                  prop.prop))
+    prop = pono.Property(s, s.make_term(And,
+                                        s.make_term(Equal, states['cfg'],
+                                                    s.make_term(0, s.make_sort(BV, 1))),
+                                        prop.prop))
 
-    kind = pono.KInduction(prop, s)
+    kind = pono.KInduction(prop, ts, s)
     res = kind.check_until(10)
 
     assert res is True, "KInduction should be able to solve this manually strengthened property"
diff --git a/tests/python/test_printers.py b/tests/python/test_printers.py
index 303b55998..92dc19246 100644
--- a/tests/python/test_printers.py
+++ b/tests/python/test_printers.py
@@ -22,10 +22,10 @@ def test_vcd_trace(create_solver):
                                 x,
                                 solver.make_term(1, x.get_sort())))
 
-    prop_term = ts.make_term(ss.primops.BVUle, x, solver.make_term(9, x.get_sort()))
+    prop_term = solver.make_term(ss.primops.BVUle, x, solver.make_term(9, x.get_sort()))
 
-    prop = pono.Property(ts, prop_term)
-    bmc = pono.Bmc(prop, solver)
+    prop = pono.Property(solver, prop_term)
+    bmc = pono.Bmc(prop, ts, solver)
     res = bmc.check_until(10)
     assert res == False, "res should be false, not just unknown (i.e. None)"
 
diff --git a/tests/test_ceg_prophecy_arrays.cpp b/tests/test_ceg_prophecy_arrays.cpp
index d42a641be..beb96f516 100644
--- a/tests/test_ceg_prophecy_arrays.cpp
+++ b/tests/test_ceg_prophecy_arrays.cpp
@@ -39,8 +39,8 @@ TEST(CegProphecyArraysTest, Simple)
 
   Term prop_term = rts.make_term(
       BVUlt, rts.make_term(Select, a, j), rts.make_term(200, bvsort32));
-  Property prop(rts, prop_term);
-  CegProphecyArrays cegp(prop, INTERP, s);
+  Property prop(s, prop_term);
+  CegProphecyArrays cegp(prop, rts, INTERP, s);
   ProverResult r = cegp.check_until(5);
   ASSERT_EQ(r, ProverResult::TRUE);
 }
diff --git a/tests/test_control_signal_modifiers.cpp b/tests/test_control_signal_modifiers.cpp
index 36d45fbc1..fc1fc33ab 100644
--- a/tests/test_control_signal_modifiers.cpp
+++ b/tests/test_control_signal_modifiers.cpp
@@ -44,9 +44,9 @@ TEST_P(ControlUnitTests, SimpleReset)
   fts.assign_next(x,
                   fts.make_term(Ite, rst, fts.make_term(0, bvsort8), x_update));
   Term p_false_term = fts.make_term(BVUle, x, fts.make_term(10, bvsort8));
-  Property p_false(fts, p_false_term);
+  Property p_false(fts.solver(), p_false_term);
   // use a new context so unroller doesn't clash on unrolled symbols
-  Bmc bmc_false(p_false, s);
+  Bmc bmc_false(p_false, fts, s);
   ProverResult r = bmc_false.check_until(2);
   EXPECT_EQ(r, ProverResult::FALSE);
 
@@ -54,12 +54,12 @@ TEST_P(ControlUnitTests, SimpleReset)
   Term reset_done = add_reset_seq(fts, rst, 1);
   // guard the property
   Term p_true_term = fts.make_term(Implies, reset_done, p_false_term);
-  Property p(fts, p_true_term);
+  Property p(fts.solver(), p_true_term);
   // need to use a fresh solver to check the property again
   // pass the SolverEnum to use the same type of solver
   SmtSolver ns = create_solver(s->get_solver_enum());
 
-  Bmc bmc(p, ns);
+  Bmc bmc(p, fts, ns);
   r = bmc.check_until(10);
   EXPECT_EQ(r,
             ProverResult::UNKNOWN);  // bmc can't prove, will only say unknown
@@ -94,21 +94,21 @@ TEST_P(ControlUnitTests, SimpleClock)
       Equal,
       x,
       rts.make_term(BVLshr, state_counter, rts.make_term(1, bvsort8)));
-  Property p_false(rts, p_term);
+  Property p_false(rts.solver(), p_term);
   // use a new context so unroller doesn't clash on unrolled symbols
-  Bmc bmc_false(p_false, s);
+  Bmc bmc_false(p_false, rts, s);
   ProverResult r = bmc_false.check_until(2);
   EXPECT_EQ(r, ProverResult::FALSE);
 
   // add a clock
   toggle_clock(rts, clk);
   // guard the property
-  Property p(rts, p_term);
+  Property p(rts.solver(), p_term);
   // need to use a fresh solver to check the property again
   // pass the SolverEnum to use the same type of solver
   SmtSolver ns = create_solver(s->get_solver_enum());
 
-  Bmc bmc(p, ns);
+  Bmc bmc(p, rts, ns);
   r = bmc.check_until(10);
   EXPECT_EQ(r,
             ProverResult::UNKNOWN);  // bmc can't prove, will only say unknown
diff --git a/tests/test_engines.cpp b/tests/test_engines.cpp
index 1e6e48ca7..220805807 100644
--- a/tests/test_engines.cpp
+++ b/tests/test_engines.cpp
@@ -51,10 +51,10 @@ class EngineUnitTests
     Term x = ts->named_terms().at("x");
 
     Term true_prop = ts->make_term(BVUle, x, ts->make_term(7, bvsort8));
-    true_p = new Property(*ts, true_prop);
+    true_p = new Property(ts->solver(), true_prop);
 
     Term false_prop = ts->make_term(BVUle, x, ts->make_term(6, bvsort8));
-    false_p = new Property(*ts, false_prop);
+    false_p = new Property(ts->solver(), false_prop);
   }
   SolverEnum se;
   Sort bvsort8;
@@ -67,7 +67,7 @@ class EngineUnitTests
 TEST_P(EngineUnitTests, BmcTrue)
 {
   SmtSolver s = create_solver(se);
-  Bmc b(*true_p, s);
+  Bmc b(*true_p, *ts, s);
   ProverResult r = b.check_until(20);
   ASSERT_EQ(r, ProverResult::UNKNOWN);
 }
@@ -75,7 +75,7 @@ TEST_P(EngineUnitTests, BmcTrue)
 TEST_P(EngineUnitTests, BmcFalse)
 {
   SmtSolver s = create_solver(se);
-  Bmc b(*false_p, s);
+  Bmc b(*false_p, *ts, s);
   ProverResult r = b.check_until(20);
   ASSERT_EQ(r, ProverResult::FALSE);
 }
@@ -83,7 +83,7 @@ TEST_P(EngineUnitTests, BmcFalse)
 TEST_P(EngineUnitTests, BmcSimplePathTrue)
 {
   SmtSolver s = create_solver(se);
-  BmcSimplePath bsp(*true_p, s);
+  BmcSimplePath bsp(*true_p, *ts, s);
   ProverResult r = bsp.check_until(20);
   ASSERT_EQ(r, ProverResult::TRUE);
 }
@@ -91,7 +91,7 @@ TEST_P(EngineUnitTests, BmcSimplePathTrue)
 TEST_P(EngineUnitTests, BmcSimplePathFalse)
 {
   SmtSolver s = create_solver(se);
-  BmcSimplePath bsp(*false_p, s);
+  BmcSimplePath bsp(*false_p, *ts, s);
   ProverResult r = bsp.check_until(20);
   ASSERT_EQ(r, ProverResult::FALSE);
 }
@@ -99,7 +99,7 @@ TEST_P(EngineUnitTests, BmcSimplePathFalse)
 TEST_P(EngineUnitTests, KInductionTrue)
 {
   SmtSolver s = create_solver(se);
-  KInduction kind(*true_p, s);
+  KInduction kind(*true_p, *ts, s);
   ProverResult r = kind.check_until(20);
   ASSERT_EQ(r, ProverResult::TRUE);
 }
@@ -107,7 +107,7 @@ TEST_P(EngineUnitTests, KInductionTrue)
 TEST_P(EngineUnitTests, KInductionFalse)
 {
   SmtSolver s = create_solver(se);
-  KInduction kind(*false_p, s);
+  KInduction kind(*false_p, *ts, s);
   ProverResult r = kind.check_until(20);
   ASSERT_EQ(r, ProverResult::FALSE);
 }
@@ -136,17 +136,17 @@ class InterpUnitTest : public EngineUnitTests
 
 TEST_P(InterpUnitTest, InterpTrue)
 {
-  InterpolantMC itpmc(*true_p, s, itp);
+  InterpolantMC itpmc(*true_p, *ts, s, itp);
   ProverResult r = itpmc.check_until(20);
   ASSERT_EQ(r, ProverResult::TRUE);
 
   Term invar = itpmc.invar();
-  ASSERT_TRUE(check_invar(true_p->transition_system(), true_p->prop(), invar));
+  ASSERT_TRUE(check_invar(*ts, true_p->prop(), invar));
 }
 
 TEST_P(InterpUnitTest, InterpFalse)
 {
-  InterpolantMC itpmc(*false_p, s, itp);
+  InterpolantMC itpmc(*false_p, *ts, s, itp);
   ProverResult r = itpmc.check_until(20);
   ASSERT_EQ(r, ProverResult::FALSE);
 }
@@ -200,7 +200,7 @@ class InterpWinTests : public ::testing::Test,
     Term witness = ts->make_statevar("witness", boolsort);
     ts->constrain_init(witness);
     ts->assign_next(witness, prop);
-    true_p = new Property(*ts, witness);
+    true_p = new Property(ts->solver(), witness);
 
     // debugging
     std::cout << "INIT" << std::endl;
@@ -219,28 +219,28 @@ class InterpWinTests : public ::testing::Test,
 
 TEST_P(InterpWinTests, BmcFail)
 {
-  Bmc b(*true_p, s);
+  Bmc b(*true_p, *ts, s);
   ProverResult r = b.check_until(10);
   ASSERT_EQ(r, ProverResult::UNKNOWN);
 }
 
 TEST_P(InterpWinTests, BmcSimplePathFail)
 {
-  BmcSimplePath bsp(*true_p, s);
+  BmcSimplePath bsp(*true_p, *ts, s);
   ProverResult r = bsp.check_until(10);
   ASSERT_EQ(r, ProverResult::UNKNOWN);
 }
 
 TEST_P(InterpWinTests, KInductionFail)
 {
-  KInduction kind(*true_p, s);
+  KInduction kind(*true_p, *ts, s);
   ProverResult r = kind.check_until(10);
   ASSERT_EQ(r, ProverResult::UNKNOWN);
 }
 
 TEST_P(InterpWinTests, InterpWin)
 {
-  InterpolantMC itpmc(*true_p, s, itp);
+  InterpolantMC itpmc(*true_p, *ts, s, itp);
   ProverResult r = itpmc.check_until(10);
   ASSERT_EQ(r, ProverResult::TRUE);
 }
diff --git a/tests/test_ic3.cpp b/tests/test_ic3.cpp
index 9aa9b9b7a..d207a1b30 100644
--- a/tests/test_ic3.cpp
+++ b/tests/test_ic3.cpp
@@ -43,9 +43,9 @@ TEST_P(IC3UnitTests, SimpleSystemSafe)
   rts.assign_next(s1, s->make_term(Or, s1, s2));
   rts.assign_next(s2, s2);
 
-  Property p(rts, s->make_term(Not, s1));
+  Property p(s, s->make_term(Not, s1));
 
-  IC3 ic3(p, s);
+  IC3 ic3(p, rts, s);
   ProverResult r = ic3.prove();
   ASSERT_EQ(r, TRUE);
 
@@ -69,9 +69,9 @@ TEST_P(IC3UnitTests, SimpleSystemUnsafe)
   fts.assign_next(s1, s->make_term(Or, s1, s2));
   fts.assign_next(s2, s2);
 
-  Property p(fts, s->make_term(Not, s1));
+  Property p(s, s->make_term(Not, s1));
 
-  IC3 ic3(p, s);
+  IC3 ic3(p, fts, s);
   ProverResult r = ic3.prove();
   ASSERT_EQ(r, FALSE);
 }
diff --git a/tests/test_ic3ia.cpp b/tests/test_ic3ia.cpp
index 26b588f60..da0dc678a 100644
--- a/tests/test_ic3ia.cpp
+++ b/tests/test_ic3ia.cpp
@@ -47,11 +47,11 @@ TEST_P(IC3IAUnitTests, SimpleSystemSafe)
   fts.assign_next(s1, s->make_term(Or, s1, s2));
   fts.assign_next(s2, s2);
 
-  Property p(fts, s->make_term(Not, s1));
+  Property p(s, s->make_term(Not, s1));
 
   SmtSolver ss = create_interpolating_solver(SolverEnum::MSAT_INTERPOLATOR);
 
-  IC3IA ic3ia(p, s, ss);
+  IC3IA ic3ia(p, fts, s, ss);
   ProverResult r = ic3ia.prove();
   ASSERT_EQ(r, TRUE);
 
@@ -75,11 +75,11 @@ TEST_P(IC3IAUnitTests, SimpleSystemUnsafe)
   fts.assign_next(s1, s->make_term(Or, s1, s2));
   fts.assign_next(s2, s2);
 
-  Property p(fts, s->make_term(Not, s1));
+  Property p(s, s->make_term(Not, s1));
 
   SmtSolver ss = create_interpolating_solver(SolverEnum::MSAT_INTERPOLATOR);
 
-  IC3IA ic3ia(p, s, ss);
+  IC3IA ic3ia(p, fts, s, ss);
   ProverResult r = ic3ia.prove();
   ASSERT_EQ(r, FALSE);
 }
@@ -93,11 +93,11 @@ TEST_P(IC3IAUnitTests, InductiveIntSafe)
 
   Term x = fts.named_terms().at("x");
 
-  Property p(fts, fts.make_term(Le, x, fts.make_term(10, intsort)));
+  Property p(fts.solver(), fts.make_term(Le, x, fts.make_term(10, intsort)));
 
   SmtSolver ss = create_interpolating_solver(SolverEnum::MSAT_INTERPOLATOR);
 
-  IC3IA ic3ia(p, s, ss);
+  IC3IA ic3ia(p, fts, s, ss);
   ProverResult r = ic3ia.prove();
   ASSERT_EQ(r, TRUE);
 
@@ -125,11 +125,11 @@ TEST_P(IC3IAUnitTests, SimpleIntSafe)
   rts.constrain_init(wit);
   rts.assign_next(wit, rts.make_term(Equal, x, y));
 
-  Property p(rts, wit);
+  Property p(rts.solver(), wit);
 
   SmtSolver ss = create_interpolating_solver(SolverEnum::MSAT_INTERPOLATOR);
 
-  IC3IA ic3ia(p, s, ss);
+  IC3IA ic3ia(p, rts, s, ss);
   ProverResult r = ic3ia.prove();
   ASSERT_EQ(r, TRUE);
 
diff --git a/tests/test_ts.cpp b/tests/test_ts.cpp
index cb204c1c3..0909c8143 100644
--- a/tests/test_ts.cpp
+++ b/tests/test_ts.cpp
@@ -123,7 +123,7 @@ TEST_P(TSUnitTests, RTS_Copy)
 TEST_P(TSUnitTests, Prop_Copy)
 {
   RelationalTransitionSystem rts(s);
-  Property p(rts, s->make_term(true));
+  Property p(s, s->make_term(true));
 
   Property p2 = p;
 }
diff --git a/tests/test_uf.cpp b/tests/test_uf.cpp
index 6d9076bcd..5ca4a6a91 100644
--- a/tests/test_uf.cpp
+++ b/tests/test_uf.cpp
@@ -60,10 +60,10 @@ TEST_P(UFUnitTests, InductiveProp)
 
   Term p = rts.make_term(
       Apply, f, rts.make_term(BVSub, x, rts.make_term(1, bvsort)));
-  Property prop(rts, p);
+  Property prop(rts.solver(), p);
 
   s->push();
-  KInduction kind(prop, s);
+  KInduction kind(prop, rts, s);
   ProverResult r = kind.check_until(5);
   EXPECT_EQ(r, ProverResult::TRUE);
   s->pop();
@@ -118,11 +118,11 @@ TEST_P(UFUnitTests, FalseProp)
       rts.make_term(
           Apply, f, rts.make_term(BVSub, x, rts.make_term(1, bvsort))));
 
-  Property prop(rts, p);
+  Property prop(rts.solver(), p);
 
   ASSERT_FALSE(rts.is_functional());
   s->push();
-  KInduction kind(prop, s);
+  KInduction kind(prop, rts, s);
   ProverResult r = kind.check_until(10);
   EXPECT_EQ(r, ProverResult::FALSE);
   s->pop();
diff --git a/tests/test_utils.cpp b/tests/test_utils.cpp
index 33e01f8dd..6a2654bf2 100644
--- a/tests/test_utils.cpp
+++ b/tests/test_utils.cpp
@@ -128,7 +128,7 @@ TEST_P(UtilsEngineUnitTests, MakeProver)
   fts.assign_next(x, fts.make_term(BVAdd, x, one));
 
   Term prop_term = fts.make_term(BVUlt, x, eight);
-  Property prop(fts, prop_term);
+  Property prop(fts.solver(), prop_term);
 
   SolverEnum se = get<0>(GetParam());
   Engine eng = get<1>(GetParam());
@@ -142,10 +142,10 @@ TEST_P(UtilsEngineUnitTests, MakeProver)
   ProverResult r;
   if (eng == INTERP && se == MSAT) {
     SmtSolver interp_s = create_interpolating_solver(MSAT_INTERPOLATOR);
-    std::shared_ptr<Prover> prover = make_prover(eng, prop, s, interp_s);
+    std::shared_ptr<Prover> prover = make_prover(eng, prop, fts, s, interp_s);
     r = prover->check_until(9);
   } else {
-    std::shared_ptr<Prover> prover = make_prover(eng, prop, s);
+    std::shared_ptr<Prover> prover = make_prover(eng, prop, fts, s);
     r = prover->check_until(9);
   }
   ASSERT_EQ(r, FALSE);
diff --git a/tests/test_witness.cpp b/tests/test_witness.cpp
index bbf0a36f3..299de7fbf 100644
--- a/tests/test_witness.cpp
+++ b/tests/test_witness.cpp
@@ -34,10 +34,10 @@ TEST_P(WitnessUnitTests, SimpleDefaultSolver)
 
   Term eight = fts.make_term(8, bvsort8);
   Term prop_term = fts.make_term(BVUlt, x, eight);
-  Property prop(fts, prop_term);
+  Property prop(fts.solver(), prop_term);
 
   SmtSolver s = create_solver(GetParam());
-  Bmc bmc(prop, s);
+  Bmc bmc(prop, fts, s);
   ProverResult r = bmc.check_until(9);
   ASSERT_EQ(r, FALSE);
 
@@ -73,10 +73,10 @@ TEST_P(WitnessUnitTests, ArraysDefaultSolver)
 
   Term ten = fts.make_term(10, bvsort8);
   Term prop_term = fts.make_term(Distinct, fts.make_term(Select, arr, x), ten);
-  Property prop(fts, prop_term);
+  Property prop(fts.solver(), prop_term);
 
   SmtSolver s = create_solver(GetParam());
-  Bmc bmc(prop, s);
+  Bmc bmc(prop, fts, s);
   ProverResult r = bmc.check_until(6);
   ASSERT_EQ(r, FALSE);