diff --git a/docs/algorithms/circuit_validator.rst b/docs/algorithms/circuit_validator.rst
index c01dd2af8..abcde6dc9 100644
--- a/docs/algorithms/circuit_validator.rst
+++ b/docs/algorithms/circuit_validator.rst
@@ -3,6 +3,10 @@ Functional equivalence of circuit nodes
 
 **Header:** ``mockturtle/algorithms/circuit_validator.hpp``
 
+This class can be used to validate potential circuit optimization choices. It checks the functional equivalence of a circuit node with an existing or non-existing signal with SAT, with optional consideration of observability don't-care (ODC).
+
+If more advanced SAT validation is needed, one could consider using ``cnf_view`` instead, which also constructs the CNF clauses of circuit nodes.
+
 **Example**
 
 The following code shows how to check functional equivalence of a root node to signals existing in the network, or created with nodes within the network. If not, get the counter example.
@@ -34,18 +38,18 @@ The following code shows how to check functional equivalence of a root node to s
       }
    }
 
-   circuit_validator<aig_network>::gate::fanin fi1;
-   fi1.idx = 0; fi1.inv = true;
-   circuit_validator<aig_network>::gate::fanin fi2;
-   fi2.idx = 1; fi2.inv = true;
-   circuit_validator<aig_network>::gate g;
-   g.fanins = {fi1, fi2};
-   g.type = circuit_validator<aig_network>::gate_type::AND;
+   circuit_validator<aig_network>::gate::fanin gi1{0, true};
+   circuit_validator<aig_network>::gate::fanin gi2{1, true};
+   circuit_validator<aig_network>::gate g{{gi1, gi2}, circuit_validator<aig_network>::gate_type::AND};
+
+   circuit_validator<aig_network>::gate::fanin hi1{2, false};
+   circuit_validator<aig_network>::gate::fanin hi2{0, false};
+   circuit_validator<aig_network>::gate h{{hi1, hi2}, circuit_validator<aig_network>::gate_type::AND};
 
-   result = v.validate( f3, {aig.get_node( f1 ), aig.get_node( f2 )}, {g}, true );
+   result = v.validate( f3, {aig.get_node( f1 ), aig.get_node( f2 )}, {g, h}, true );
    if ( result && *result )
    {
-     std::cout << "f3 is equivalent to NOT(NOT f1 AND NOT f2)\n";
+     std::cout << "f3 is equivalent to NOT((NOT f1 AND NOT f2) AND f1)\n";
    }
 
 **Parameters**
@@ -70,9 +74,8 @@ The following code shows how to check functional equivalence of a root node to s
 .. doxygenstruct:: mockturtle::circuit_validator::gate
    :members: fanins, type
 .. doxygenstruct:: mockturtle::circuit_validator::gate::fanin
-   :members: idx, inv
+   :members: index, inverted
 
 **Updating**
 
-.. doxygenfunction:: mockturtle::circuit_validator::add_node
 .. doxygenfunction:: mockturtle::circuit_validator::update
diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp
index c1c8437f4..d2eae5139 100644
--- a/include/mockturtle/algorithms/circuit_validator.hpp
+++ b/include/mockturtle/algorithms/circuit_validator.hpp
@@ -44,6 +44,9 @@ namespace mockturtle
 
 struct validator_params
 {
+  /*! \brief Maximum number of clauses of the SAT solver. (incremental CNF construction) */
+  uint32_t max_clauses{1000};
+
   /*! \brief Whether to consider ODC, and how many levels. 0 = No consideration. -1 = Consider TFO until PO. */
   int odc_levels{0};
 
@@ -73,11 +76,11 @@ class circuit_validator
   {
     struct fanin
     {
-      /*! \brief Index in the concatenated list of `divs` and `ckt`. */
-      uint32_t idx;
+      /*! \brief Index in the concatenated list of `divs` and `circuit`. */
+      uint32_t index;
 
       /*! \brief Input negation. */
-      bool inv{false};
+      bool inverted{false};
     };
 
     /*! \brief Fanins of the gate. */
@@ -137,58 +140,85 @@ class circuit_validator
   /*! \brief Validate functional equivalence of signals `f` and `d`. */
   std::optional<bool> validate( signal const& f, signal const& d )
   {
-    return validate( ntk.get_node( f ), lit_not_cond( literals[d], ntk.is_complemented( f ) ^ ntk.is_complemented( d ) ) );
+    if ( !literals.has( d ) )
+    {
+      construct( ntk.get_node( d ) );
+    }
+    auto const res = validate( ntk.get_node( f ), lit_not_cond( literals[d], ntk.is_complemented( f ) ^ ntk.is_complemented( d ) ) );
+    if ( solver.num_clauses() > ps.max_clauses )
+    {
+      restart();
+    }
+    return res;
   }
 
   /*! \brief Validate functional equivalence of node `root` and signal `d`. */
   std::optional<bool> validate( node const& root, signal const& d )
   {
-    return validate( root, lit_not_cond( literals[d], ntk.is_complemented( d ) ) );
+    if ( !literals.has( d ) )
+    {
+      construct( ntk.get_node( d ) );
+    }
+    auto const res = validate( root, lit_not_cond( literals[d], ntk.is_complemented( d ) ) );
+    if ( solver.num_clauses() > ps.max_clauses )
+    {
+      restart();
+    }
+    return res;
   }
 
   /*! \brief Validate functional equivalence of signal `f` with a circuit.
    * 
-   * The circuit `ckt` uses `divs` as inputs, which are existing nodes in the network.
+   * The circuit `circuit` uses `divs` as inputs, which are existing nodes in the network.
    *
-   * \param divs Existing nodes in the network, serving as PIs of `ckt`.
-   * \param ckt Circuit built with `divs` as inputs. Please see the documentation of `circuit_validator::gate` for its data structure.
+   * \param divs Existing nodes in the network, serving as PIs of `circuit`.
+   * \param circuit Circuit built with `divs` as inputs. Please see the documentation of `circuit_validator::gate` for its data structure.
    * \param output_negation Output negation of the topmost gate of the circuit.
    */
-  std::optional<bool> validate( signal const& f, std::vector<node> const& divs, std::vector<gate> const& ckt, bool output_negation = false )
+  std::optional<bool> validate( signal const& f, std::vector<node> const& divs, std::vector<gate> const& circuit, bool output_negation = false )
   {
-    return validate( ntk.get_node( f ), divs.begin(), divs.end(), ckt, output_negation ^ ntk.is_complemented( f ) );
+    return validate( ntk.get_node( f ), divs.begin(), divs.end(), circuit, output_negation ^ ntk.is_complemented( f ) );
   }
 
   /*! \brief Validate functional equivalence of node `root` with a circuit. */
-  std::optional<bool> validate( node const& root, std::vector<node> const& divs, std::vector<gate> const& ckt, bool output_negation = false )
+  std::optional<bool> validate( node const& root, std::vector<node> const& divs, std::vector<gate> const& circuit, bool output_negation = false )
   {
-    return validate( root, divs.begin(), divs.end(), ckt, output_negation );
+    return validate( root, divs.begin(), divs.end(), circuit, output_negation );
   }
 
   /*! \brief Validate functional equivalence of signal `f` with a circuit. */
   template<class iterator_type>
-  std::optional<bool> validate( signal const& f, iterator_type divs_begin, iterator_type divs_end, std::vector<gate> const& ckt, bool output_negation = false )
+  std::optional<bool> validate( signal const& f, iterator_type divs_begin, iterator_type divs_end, std::vector<gate> const& circuit, bool output_negation = false )
   {
-    return validate( ntk.get_node( f ), divs_begin, divs_end, ckt, output_negation ^ ntk.is_complemented( f ) );
+    return validate( ntk.get_node( f ), divs_begin, divs_end, circuit, output_negation ^ ntk.is_complemented( f ) );
   }
 
   /*! \brief Validate functional equivalence of node `root` with a circuit. */
   template<class iterator_type>
-  std::optional<bool> validate( node const& root, iterator_type divs_begin, iterator_type divs_end, std::vector<gate> const& ckt, bool output_negation = false )
+  std::optional<bool> validate( node const& root, iterator_type divs_begin, iterator_type divs_end, std::vector<gate> const& circuit, bool output_negation = false )
   {
-    if constexpr ( use_pushpop )
+    if ( !literals.has( root ) )
     {
-      solver.push();
+      construct( root );
     }
 
     std::vector<bill::lit_type> lits;
     while ( divs_begin != divs_end )
     {
+      if ( !literals.has( *divs_begin ) )
+      {
+        construct( *divs_begin );
+      }
       lits.emplace_back( literals[*divs_begin] );
       divs_begin++;
     }
 
-    for ( auto g : ckt )
+    if constexpr ( use_pushpop )
+    {
+      solver.push();
+    }
+
+    for ( auto g : circuit )
     {
       lits.emplace_back( add_tmp_gate( lits, g ) );
     }
@@ -200,6 +230,11 @@ class circuit_validator
       solver.pop();
     }
 
+    if ( solver.num_clauses() > ps.max_clauses )
+    {
+      restart();
+    }
+
     return res;
   }
 
@@ -212,18 +247,26 @@ class circuit_validator
   /*! \brief Validate whether node `root` is a constant of `value`. */
   std::optional<bool> validate( node const& root, bool value )
   {
-    assert( literals[root].variable() != bill::var_type( 0 ) );
-    if constexpr ( use_pushpop )
+    if ( !literals.has( root ) )
     {
-      solver.push();
+      construct( root );
     }
+    assert( literals[root].variable() != bill::var_type( 0 ) );
 
     std::optional<bool> res;
     if constexpr ( use_odc )
     {
       if ( ps.odc_levels != 0 )
       {
+        if constexpr ( use_pushpop )
+        {
+          solver.push();
+        }
         res = solve( {build_odc_window( root, ~literals[root] ), lit_not_cond( literals[root], value )} );
+        if constexpr ( use_pushpop )
+        {
+          solver.pop();
+        }
       }
       else
       {
@@ -235,41 +278,13 @@ class circuit_validator
       res = solve( {lit_not_cond( literals[root], value )} );
     }
 
-    if constexpr ( use_pushpop )
+    if ( solver.num_clauses() > ps.max_clauses )
     {
-      solver.pop();
+      restart();
     }
     return res;
   }
 
-  /*! \brief Add CNF clauses for a newly created node.
-   *
-   * This function should be called when a new node is created after 
-   * construction of circuit_validator.
-   * It can be called manually every time or be added to `ntk.on_add` events.
-   */
-  void add_node( node const& n )
-  {
-    std::vector<bill::lit_type> lit_fi;
-    ntk.foreach_fanin( n, [&]( const auto& f ) {
-      lit_fi.emplace_back( lit_not_cond( literals[f], ntk.is_complemented( f ) ) );
-    } );
-
-    literals.resize();
-    assert( lit_fi.size() == 2u || lit_fi.size() == 3u );
-    if ( lit_fi.size() == 2u )
-    {
-      assert( ntk.is_and( n ) || ntk.is_xor( n ) );
-      literals[n] = add_clauses_for_2input_gate( lit_fi[0], lit_fi[1], std::nullopt, ntk.is_and( n ) ? AND : XOR );
-    }
-    else
-    {
-      assert( lit_fi.size() == 3u );
-      assert( ntk.is_maj( n ) || ntk.is_xor3( n ) );
-      literals[n] = add_clauses_for_3input_gate( lit_fi[0], lit_fi[1], lit_fi[2], std::nullopt, ntk.is_maj( n ) ? MAJ : XOR );
-    }
-  }
-
   /*! \brief Update CNF clauses.
    *
    * This function should be called when the function of one or more nodes
@@ -303,17 +318,59 @@ class circuit_validator
     } );
 
     /* compute literals for nodes */
-    uint32_t next_var = ntk.num_pis() + 1;
-    ntk.foreach_gate( [&]( auto const& n ) {
-      literals[n] = bill::lit_type( next_var++, bill::lit_type::polarities::positive );
+    //uint32_t next_var = ntk.num_pis() + 1;
+    //ntk.foreach_gate( [&]( auto const& n ) {
+    //  literals[n] = bill::lit_type( next_var++, bill::lit_type::polarities::positive );
+    //} );
+
+    solver.add_variables( ntk.num_pis() + 1 );
+    solver.add_clause( {~literals[ntk.get_constant( false )]} );
+
+    //generate_cnf<Ntk, bill::lit_type>(
+    //    ntk, [&]( auto const& clause ) {
+    //      solver.add_clause( clause );
+    //    },
+    //    literals );
+  }
+
+  void construct( node const& n )
+  {
+    assert( !literals.has( n ) );
+
+    std::vector<bill::lit_type> child_lits;
+    ntk.foreach_fanin( n, [&]( auto const& f ) {
+      if ( !literals.has( f ) )
+      {
+        construct( ntk.get_node( f ) );
+      }
+      child_lits.push_back( lit_not_cond( literals[f], ntk.is_complemented( f ) ) );
     } );
+    bill::lit_type node_lit = literals[n] = bill::lit_type( solver.add_variable(), bill::lit_type::polarities::positive );
 
-    solver.add_variables( ntk.size() );
-    generate_cnf<Ntk, bill::lit_type>(
-        ntk, [&]( auto const& clause ) {
-          solver.add_clause( clause );
-        },
-        literals );
+    if ( ntk.is_and( n ) )
+    {
+      detail::on_and<add_clause_fn_t>( node_lit, child_lits[0], child_lits[1], [&]( auto const& clause ) {
+        solver.add_clause( clause );
+      } );
+    }
+    else if ( ntk.is_xor( n ) )
+    {
+      detail::on_xor<add_clause_fn_t>( node_lit, child_lits[0], child_lits[1], [&]( auto const& clause ) {
+        solver.add_clause( clause );
+      } );
+    }
+    else if ( ntk.is_xor3( n ) )
+    {
+      detail::on_xor3<add_clause_fn_t>( node_lit, child_lits[0], child_lits[1], child_lits[2], [&]( auto const& clause ) {
+        solver.add_clause( clause );
+      } );
+    }
+    else if ( ntk.is_maj( n ) )
+    {
+      detail::on_maj<add_clause_fn_t>( node_lit, child_lits[0], child_lits[1], child_lits[2], [&]( auto const& clause ) {
+        solver.add_clause( clause );
+      } );
+    }
   }
 
   bill::lit_type add_clauses_for_2input_gate( bill::lit_type a, bill::lit_type b, std::optional<bill::lit_type> c = std::nullopt, gate_type type = AND )
@@ -365,22 +422,23 @@ class circuit_validator
 
     if ( g.fanins.size() == 2u )
     {
-      assert( g.fanins[0].idx < lits.size() );
-      assert( g.fanins[1].idx < lits.size() );
-      return add_clauses_for_2input_gate( lit_not_cond( lits[g.fanins[0].idx], g.fanins[0].inv ), lit_not_cond( lits[g.fanins[1].idx], g.fanins[1].inv ), std::nullopt, g.type );
+      assert( g.fanins[0].index < lits.size() );
+      assert( g.fanins[1].index < lits.size() );
+      return add_clauses_for_2input_gate( lit_not_cond( lits[g.fanins[0].index], g.fanins[0].inverted ), lit_not_cond( lits[g.fanins[1].index], g.fanins[1].inverted ), std::nullopt, g.type );
     }
     else
     {
-      assert( g.fanins[0].idx < lits.size() );
-      assert( g.fanins[1].idx < lits.size() );
-      assert( g.fanins[2].idx < lits.size() );
-      return add_clauses_for_3input_gate( lit_not_cond( lits[g.fanins[0].idx], g.fanins[0].inv ), lit_not_cond( lits[g.fanins[1].idx], g.fanins[1].inv ), lit_not_cond( lits[g.fanins[2].idx], g.fanins[2].inv ), std::nullopt, g.type );
+      assert( g.fanins[0].index < lits.size() );
+      assert( g.fanins[1].index < lits.size() );
+      assert( g.fanins[2].index < lits.size() );
+      return add_clauses_for_3input_gate( lit_not_cond( lits[g.fanins[0].index], g.fanins[0].inverted ), lit_not_cond( lits[g.fanins[1].index], g.fanins[1].inverted ), lit_not_cond( lits[g.fanins[2].index], g.fanins[2].inverted ), std::nullopt, g.type );
     }
   }
 
   std::optional<bool> solve( std::vector<bill::lit_type> assumptions )
   {
     auto const res = solver.solve( assumptions, ps.conflict_limit );
+
     if ( res == bill::result::states::satisfiable )
     {
       auto model = solver.get_model().model();
@@ -399,18 +457,26 @@ class circuit_validator
 
   std::optional<bool> validate( node const& root, bill::lit_type const& lit )
   {
-    assert( literals[root].variable() != bill::var_type( 0 ) );
-    if constexpr ( use_pushpop )
+    if ( !literals.has( root ) )
     {
-      solver.push();
+      construct( root );
     }
+    assert( literals[root].variable() != bill::var_type( 0 ) );
 
     std::optional<bool> res;
     if constexpr ( use_odc )
     {
       if ( ps.odc_levels != 0 )
       {
+        if constexpr ( use_pushpop )
+        {
+          solver.push();
+        }
         res = solve( {build_odc_window( root, lit )} );
+        if constexpr ( use_pushpop )
+        {
+          solver.pop();
+        }
       }
       else
       {
@@ -428,10 +494,6 @@ class circuit_validator
       res = solve( {~nlit} );
     }
 
-    if constexpr ( use_pushpop )
-    {
-      solver.pop();
-    }
     return res;
   }
 
@@ -475,6 +537,10 @@ class circuit_validator
 
       std::vector<bill::lit_type> l_fi;
       ntk.foreach_fanin( fo, [&]( auto const& fi ) {
+        if ( !literals.has( fi ) )
+        {
+          construct( ntk.get_node( fi ) );
+        }
         l_fi.emplace_back( lit_not_cond( lits.has( ntk.get_node( fi ) ) ? lits[fi] : literals[fi], ntk.is_complemented( fi ) ) );
       } );
       if ( l_fi.size() == 2u )
@@ -529,7 +595,7 @@ class circuit_validator
 
   validator_params const& ps;
 
-  node_map<bill::lit_type, Ntk> literals;
+  unordered_node_map<bill::lit_type, Ntk> literals;
   bill::solver<Solver> solver;
 
 public:
diff --git a/include/mockturtle/utils/node_map.hpp b/include/mockturtle/utils/node_map.hpp
index f4595feca..3367e58e5 100644
--- a/include/mockturtle/utils/node_map.hpp
+++ b/include/mockturtle/utils/node_map.hpp
@@ -232,6 +232,12 @@ class node_map<T, Ntk, std::unordered_map<typename Ntk::node, T>>
     return data->find( ntk.node_to_index( n ) ) != data->end();
   }
 
+  /*! \brief Check if a key is already defined. */
+  bool has( signal const& f ) const
+  {
+    return data->find( ntk.node_to_index( ntk.get_node( f ) ) ) != data->end();
+  }
+
   /*! \brief Mutable access to value by node. */
   reference operator[]( node const& n )
   {
diff --git a/lib/abcsat/abc/satSolver.h b/lib/abcsat/abc/satSolver.h
index 948f6442a..bedc6dc81 100644
--- a/lib/abcsat/abc/satSolver.h
+++ b/lib/abcsat/abc/satSolver.h
@@ -310,6 +310,12 @@ static inline int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
 
 static inline void sat_solver_bookmark(sat_solver* s)
 {
+    if (s->qtail != s->qhead)
+    {
+        int status = sat_solver_simplify(s);
+        assert(status!=0);
+        assert(s->qtail == s->qhead);
+    }
     assert( s->qhead == s->qtail );
     s->iVarPivot    = s->size;
     s->iTrailPivot  = s->qhead;
diff --git a/lib/bill/bill/sat/interface/abc_bsat2.hpp b/lib/bill/bill/sat/interface/abc_bsat2.hpp
index 043bb6f09..8f5d6f7e8 100644
--- a/lib/bill/bill/sat/interface/abc_bsat2.hpp
+++ b/lib/bill/bill/sat/interface/abc_bsat2.hpp
@@ -8,9 +8,9 @@
 #include "types.hpp"
 
 #include <memory>
+#include <random>
 #include <variant>
 #include <vector>
-#include <random>
 
 namespace bill {
 
@@ -21,6 +21,8 @@ class solver<solvers::bsat2> {
 public:
 #pragma region Constructors
 	solver()
+	    : variable_counter(1, 0u)
+	    , clause_counter(1, 0)
 	{
 		solver_ = pabc::sat_solver_new();
 	}
@@ -42,15 +44,21 @@ class solver<solvers::bsat2> {
 		pabc::sat_solver_restart(solver_);
 		state_ = result::states::undefined;
 		randomize = false;
+		variable_counter.clear();
+		variable_counter.emplace_back(0u);
+		clause_counter.clear();
+		clause_counter.emplace_back(0);
 	}
 
 	var_type add_variable()
 	{
+		++variable_counter.back();
 		return pabc::sat_solver_addvar(solver_);
 	}
 
 	void add_variables(uint32_t num_variables = 1)
 	{
+		variable_counter.back() += num_variables;
 		for (auto i = 0u; i < num_variables; ++i) {
 			pabc::sat_solver_addvar(solver_);
 		}
@@ -59,6 +67,7 @@ class solver<solvers::bsat2> {
 	auto add_clause(std::vector<lit_type>::const_iterator it,
 	                std::vector<lit_type>::const_iterator ie)
 	{
+		++clause_counter.back();
 		auto counter = 0u;
 		while (it != ie) {
 			literals[counter++] = pabc::Abc_Var2Lit(it->variable(),
@@ -77,6 +86,7 @@ class solver<solvers::bsat2> {
 
 	auto add_clause(lit_type lit)
 	{
+		--clause_counter.back(); /* do not count unit clauses */
 		return add_clause(std::vector<lit_type>{lit});
 	}
 
@@ -112,17 +122,16 @@ class solver<solvers::bsat2> {
 		if (num_variables() == 0u)
 			return result::states::undefined;
 
-		if ( randomize )
-		{
+		if (randomize) {
 			std::vector<uint32_t> vars;
-			for ( auto i = 0u; i < num_variables(); ++i )
-			{
-				if ( random() % 2 )
-				{
-					vars.push_back( i );
+			for (auto i = 0u; i < num_variables(); ++i) {
+				if (random() % 2) {
+					vars.push_back(i);
 				}
 			}
-			pabc::sat_solver_set_polarity( solver_, (int*)(const_cast<uint32_t*>(vars.data())), vars.size() );
+			pabc::sat_solver_set_polarity(solver_,
+			                              (int*) (const_cast<uint32_t*>(vars.data())),
+			                              vars.size());
 		}
 
 		int result;
@@ -157,31 +166,37 @@ class solver<solvers::bsat2> {
 #pragma region Properties
 	uint32_t num_variables() const
 	{
-		return pabc::sat_solver_nvars(solver_);
+		return variable_counter.back();
+		/* Note: `pabc::sat_solver_nvars(solver_)` is not correct when bookmark/rollback is used */
 	}
 
 	uint32_t num_clauses() const
 	{
-		return pabc::sat_solver_nclauses(solver_);
+		return clause_counter.back();
+		/* Note: `pabc::sat_solver_nclauses(solver_)` is not correct when bookmark/rollback is used */
 	}
 #pragma endregion
 
 	void push()
 	{
 		pabc::sat_solver_bookmark(solver_);
+		variable_counter.emplace_back(variable_counter.back());
+		clause_counter.emplace_back(clause_counter.back());
 	}
 
-	void pop( uint32_t n = 1u )
+	void pop(uint32_t num_levels = 1u)
 	{
-		assert( n == 1u && "bsat does not support multiple step pop" ); (void)n;
-	    pabc::sat_solver_rollback(solver_);
+		assert(num_levels == 1u && "bsat does not support multiple step pop");
+		pabc::sat_solver_rollback(solver_);
+		variable_counter.resize(variable_counter.size() - num_levels);
+		clause_counter.resize(clause_counter.size() - num_levels);
 	}
 
-	void set_random_phase( uint32_t seed = 0u )
+	void set_random_phase(uint32_t seed = 0u)
 	{
 		randomize = true;
 		pabc::sat_solver_set_random(solver_, 1);
-		random.seed( seed );
+		random.seed(seed);
 	}
 
 private:
@@ -194,8 +209,15 @@ class solver<solvers::bsat2> {
 	/*! \brief Temporary storage for one clause */
 	pabc::lit literals[2048];
 
-	std::default_random_engine random;
+	/*! \brief Whether to randomize initial variable values */
 	bool randomize = false;
+	std::default_random_engine random;
+
+	/*! \brief Stacked counter for number of variables */
+	std::vector<uint32_t> variable_counter;
+
+	/*! \brief Stacked counter for number of clauses */
+	std::vector<int> clause_counter;
 };
 
 } // namespace bill
diff --git a/lib/bill/bill/sat/interface/z3.hpp b/lib/bill/bill/sat/interface/z3.hpp
index bdae5103a..f68772799 100644
--- a/lib/bill/bill/sat/interface/z3.hpp
+++ b/lib/bill/bill/sat/interface/z3.hpp
@@ -21,9 +21,10 @@ class solver<solvers::z3> {
 public:
 #pragma region Constructors
 	solver()
-	    : solver_(ctx_), var_ctr_( 1, 0u ), cls_ctr_( 1, 0u )
-	{
-	}
+	    : solver_(ctx_)
+	    , variable_counter_(1, 0u)
+	    , clause_counter_(1, 0u)
+	{}
 
 	~solver()
 	{}
@@ -38,17 +39,17 @@ class solver<solvers::z3> {
 	{
 		solver_.reset();
 		vars_.clear();
-		var_ctr_.clear();
-		var_ctr_.emplace_back( 0u );
-		cls_ctr_.clear();
-		cls_ctr_.emplace_back( 0u );
+		variable_counter_.clear();
+		variable_counter_.emplace_back(0u);
+		clause_counter_.clear();
+		clause_counter_.emplace_back(0u);
 		state_ = result::states::undefined;
 	}
 
 	var_type add_variable()
 	{
-		vars_.push_back(ctx_.bool_const(fmt::format("x{}", var_ctr_.back()).c_str()));
-		return var_ctr_.back()++;
+		vars_.push_back(ctx_.bool_const(fmt::format("x{}", variable_counter_.back()).c_str()));
+		return variable_counter_.back()++;
 	}
 
 	void add_variables(uint32_t num_variables = 1)
@@ -68,7 +69,7 @@ class solver<solvers::z3> {
 			++it;
 		}
 		solver_.add(mk_or(vec));
-		++cls_ctr_.back();
+		++clause_counter_.back();
 		return result::states::dirty;
 	}
 
@@ -112,7 +113,9 @@ class solver<solvers::z3> {
 		for (auto const& lit : assumptions)
 			vec.push_back(lit.is_complemented() ? !vars_[lit.variable()] :
 			                                      vars_[lit.variable()]);
-		solver_.set("sat.max_conflicts", conflict_limit == 0u ? std::numeric_limits<uint32_t>::max() : conflict_limit);
+		solver_.set("sat.max_conflicts", conflict_limit == 0u ?
+		                                     std::numeric_limits<uint32_t>::max() :
+		                                     conflict_limit);
 		switch (solver_.check(vec)) {
 		case z3::sat:
 			state_ = result::states::satisfiable;
@@ -133,47 +136,57 @@ class solver<solvers::z3> {
 #pragma region Properties
 	uint32_t num_variables() const
 	{
-		return var_ctr_.back();
+		return variable_counter_.back();
 	}
 
 	uint32_t num_clauses() const
 	{
-		return cls_ctr_.back();
+		return clause_counter_.back();
 	}
 #pragma endregion
 
 	void push()
 	{
 		solver_.push();
-		var_ctr_.emplace_back( var_ctr_.back() );
-		cls_ctr_.emplace_back( cls_ctr_.back() );
+		variable_counter_.emplace_back(variable_counter_.back());
+		clause_counter_.emplace_back(clause_counter_.back());
 	}
 
-	void pop( uint32_t n = 1u )
+	void pop(uint32_t num_levels = 1u)
 	{
-		assert( n < var_ctr_.size() );
-		solver_.pop( n );
-		var_ctr_.resize( var_ctr_.size() - n );
-		cls_ctr_.resize( cls_ctr_.size() - n );
-		if ( vars_.size() > var_ctr_.back() )
-		{
-			vars_.erase( vars_.begin() + var_ctr_.back(), vars_.end() );
+		assert(num_levels < variable_counter_.size());
+		solver_.pop(num_levels);
+		variable_counter_.resize(variable_counter_.size() - num_levels);
+		clause_counter_.resize(clause_counter_.size() - num_levels);
+		if (vars_.size() > variable_counter_.back()) {
+			vars_.erase(vars_.begin() + variable_counter_.back(), vars_.end());
 		}
 	}
 
-	void set_random_phase( uint32_t seed = 0u )
+	void set_random_phase(uint32_t seed = 0u)
 	{
 		solver_.set("sat.random_seed", seed);
 		solver_.set("phase_selection", 5u);
 	}
 
 private:
+	/*! \brief Backend solver context object */
 	z3::context ctx_;
+
+	/*! \brief Backend solver */
 	z3::solver solver_;
+
+	/*! \brief Current state of the solver */
 	result::states state_ = result::states::undefined;
+
+	/*! \brief Variables */
 	std::vector<z3::expr> vars_;
-	std::vector<uint32_t> var_ctr_;
-	std::vector<uint32_t> cls_ctr_;
+
+	/*! \brief Stacked counter for number of variables */
+	std::vector<uint32_t> variable_counter_;
+
+	/*! \brief Stacked counter for number of clauses */
+	std::vector<uint32_t> clause_counter_;
 };
 
 } // namespace bill
diff --git a/lib/bill/bill/sat/solver/abc/satSolver.h b/lib/bill/bill/sat/solver/abc/satSolver.h
index df3626654..dd8d32b85 100644
--- a/lib/bill/bill/sat/solver/abc/satSolver.h
+++ b/lib/bill/bill/sat/solver/abc/satSolver.h
@@ -310,6 +310,12 @@ static inline int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
 
 static inline void sat_solver_bookmark(sat_solver* s)
 {
+    if (s->qtail != s->qhead)
+    {
+        int status = sat_solver_simplify(s);
+        assert(status!=0);
+        assert(s->qtail == s->qhead);
+    }
     assert( s->qhead == s->qtail );
     s->iVarPivot    = s->size;
     s->iTrailPivot  = s->qhead;
diff --git a/test/algorithms/circuit_validator.cpp b/test/algorithms/circuit_validator.cpp
index a54d40ff7..dfef6c0cd 100644
--- a/test/algorithms/circuit_validator.cpp
+++ b/test/algorithms/circuit_validator.cpp
@@ -71,12 +71,10 @@ TEST_CASE( "Validating with non-existing circuit", "[validator]" )
 
   circuit_validator v( aig );
 
-  circuit_validator<aig_network>::gate::fanin fi1;
-  fi1.idx = 0; fi1.inv = true;
-  circuit_validator<aig_network>::gate::fanin fi2;
-  fi2.idx = 1; fi2.inv = true;
-  circuit_validator<aig_network>::gate g;
-  g.fanins = {fi1, fi2};
+  circuit_validator<aig_network>::gate::fanin gi1{0, true};
+  circuit_validator<aig_network>::gate::fanin gi2{1, true};
+  circuit_validator<aig_network>::gate g{{gi1, gi2}, circuit_validator<aig_network>::gate_type::AND};
+
   CHECK( *( v.validate( f3, {aig.get_node( f1 ), aig.get_node( f2 )}, {g}, true ) ) == true );
   CHECK( *( v.validate( aig.get_node( f3 ), {aig.get_node( f1 ), aig.get_node( f2 )}, {g}, false ) ) == true );
 }
@@ -93,13 +91,9 @@ TEST_CASE( "Validating after circuit update", "[validator]" )
 
   circuit_validator v( aig );
 
-  /* new nodes created after construction of `circuit_validator` have to be added to it manually with `add_node` */
   auto const g1 = aig.create_and( a, b );
   auto const g2 = aig.create_and( !a, !b );
   auto const g3 = aig.create_or( g1, g2 );
-  v.add_node( aig.get_node( g1 ) );
-  v.add_node( aig.get_node( g2 ) );
-  v.add_node( aig.get_node( g3 ) );
 
   CHECK( *( v.validate( aig.get_node( f3 ), g3 ) ) == true );
 }