diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp
index 1196b27ff..1ee68890e 100644
--- a/libsmtutil/Z3CHCInterface.cpp
+++ b/libsmtutil/Z3CHCInterface.cpp
@@ -80,6 +80,7 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
 pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
 {
 	CheckResult result;
+	cout << m_solver << endl;
 	try
 	{
 		z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 7cc963956..a568aaa46 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -756,14 +756,14 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	for (auto var: function->returnParameters())
 		m_context.variable(*var)->increaseIndex();
 
-	auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
+	auto preCallState = /*vector<smtutil::Expression>{state().state()} + */currentStateVariables();
 	bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
 		function->stateMutability() == StateMutability::Pure ||
 		function->stateMutability() == StateMutability::View;
 
 	if (!usesStaticCall)
 	{
-		state().newState();
+		//state().newState();
 		for (auto const* var: m_stateVariables)
 			m_context.variable(*var)->increaseIndex();
 	}
@@ -776,8 +776,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 		PredicateType::ExternalCallUntrusted,
 		&_funCall
 	);
-	auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
-	vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
+	auto postCallState = /*vector<smtutil::Expression>{state().state()} +*/ currentStateVariables();
+	vector<smtutil::Expression> stateExprs{error, state().thisAddress()/*, state().abi(), state().crypto()*/};
 
 	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
 	auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
@@ -809,21 +809,21 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 		return;
 
 	// External call creates a new transaction.
-	auto originalTx = state().tx();
-	auto txOrigin = state().txMember("tx.origin");
-	state().newTx();
+	//auto originalTx = state().tx();
+	//auto txOrigin = state().txMember("tx.origin");
+	//state().newTx();
 	// set the transaction sender as this contract
-	m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
+	//m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
 	// set the origin to be the current transaction origin
-	m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
+	//m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
 
 	smtutil::Expression pred = predicate(_funCall);
 
 	auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function);
 	m_context.addAssertion(pred && txConstraints);
 	// restore the original transaction data
-	state().newTx();
-	m_context.addAssertion(originalTx == state().tx());
+	//state().newTx();
+	//m_context.addAssertion(originalTx == state().tx());
 
 	solAssert(m_errorDest, "");
 	connectBlocks(
@@ -1002,7 +1002,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 			m_context.variable(*var)->increaseIndex();
 	}
 
-	state().newState();
+	//state().newState();
 }
 
 void CHC::setCurrentBlock(Predicate const& _block)
@@ -1125,10 +1125,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 					auto errorPost = errorFlag().increaseIndex();
 					auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
 
-					vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
+					vector<smtutil::Expression> args{errorPost, state().thisAddress()/*, state().abi(), state().crypto(), state().tx(), state().state(1)*/};
 					args += state1 +
 						applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
-						vector<smtutil::Expression>{state().state(2)} +
+						//vector<smtutil::Expression>{state().state(2)} +
 						state2 +
 						applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
 						applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
@@ -1272,7 +1272,7 @@ void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression co
 
 smtutil::Expression CHC::initialConstraints(ContractDefinition const& _contract, FunctionDefinition const* _function)
 {
-	smtutil::Expression conj = state().state() == state().state(0);
+	smtutil::Expression conj(true);// = state().state() == state().state(0);
 	conj = conj && errorFlag().currentValue() == 0;
 	conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_contract));
 
@@ -1387,7 +1387,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		solAssert(false, "Unreachable!");
 	};
 	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
+	vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall)/*, state().abi(), state().crypto(), state().tx(), state().state()*/};
 
 	auto const* contract = function->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
@@ -1399,11 +1399,11 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	args += symbolicArguments(_funCall, m_currentContract);
 	if (!m_currentContract->isLibrary() && !usesStaticCall)
 	{
-		state().newState();
+		//state().newState();
 		for (auto const& var: m_stateVariables)
 			m_context.variable(*var)->increaseIndex();
 	}
-	args += vector<smtutil::Expression>{state().state()};
+	//args += vector<smtutil::Expression>{state().state()};
 	args += currentStateVariables(*m_currentContract);
 
 	for (auto var: function->parameters() + function->returnParameters())
@@ -1660,6 +1660,7 @@ void CHC::checkAndReportTarget(
 	else if (result == CheckResult::SATISFIABLE)
 	{
 		solAssert(!_satMsg.empty(), "");
+		/*
 		auto cex = generateCounterexample(model, error().name);
 		if (cex)
 			m_unsafeTargets[_target.errorNode][_target.type] = {
@@ -1668,6 +1669,7 @@ void CHC::checkAndReportTarget(
 				"CHC: " + _satMsg + "\nCounterexample:\n" + *cex
 			};
 		else
+		*/
 			m_unsafeTargets[_target.errorNode][_target.type] = {
 				_errorReporterId,
 				location,
diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp
index aff6aa19b..29982ff37 100644
--- a/libsolidity/formal/PredicateInstance.cpp
+++ b/libsolidity/formal/PredicateInstance.cpp
@@ -30,14 +30,14 @@ namespace solidity::frontend::smt
 smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)};
+	vector<smtutil::Expression> stateExprs{state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.state(0)*/};
 	return _pred(stateExprs + initialStateVariables(_contract, _context));
 }
 
 smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
 {
 	auto const& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.state()*/};
 	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
@@ -49,12 +49,12 @@ smtutil::Expression nondetInterface(
 	unsigned _postIdx)
 {
 	auto const& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress()/*, state.abi(), state.crypto()*/};
 	return _pred(
 		stateExprs +
-		vector<smtutil::Expression>{_context.state().state(_preIdx)} +
+		//vector<smtutil::Expression>{_context.state().state(_preIdx)} +
 		stateVariablesAtIndex(_preIdx, _contract, _context) +
-		vector<smtutil::Expression>{_context.state().state(_postIdx)} +
+		//vector<smtutil::Expression>{_context.state().state(_postIdx)} +
 		stateVariablesAtIndex(_postIdx, _contract, _context)
 	);
 }
@@ -66,7 +66,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
 		return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()*/};
 	return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
 }
 
@@ -77,9 +77,9 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co
 		return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
-	state.newState();
-	stateExprs += vector<smtutil::Expression>{state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.tx(0), state.state()*/};
+	//state.newState();
+	//stateExprs += vector<smtutil::Expression>{state.state()};
 	stateExprs += currentStateVariables(contract, _context);
 	stateExprs += newStateVariables(contract, _context);
 	return _pred(stateExprs);
@@ -153,10 +153,10 @@ vector<smtutil::Expression> currentFunctionVariablesForDefinition(
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)};
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.tx(0), state.state(0)*/};
 	exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
-	exprs += vector<smtutil::Expression>{state.state()};
+	//exprs += vector<smtutil::Expression>{state.state()};
 	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
 	exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
@@ -170,13 +170,13 @@ vector<smtutil::Expression> currentFunctionVariablesForCall(
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0)/*, state.abi(0), state.crypto(0), state.tx(0), state.state()*/};
 	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
 
-	state.newState();
+	//state.newState();
 
-	exprs += vector<smtutil::Expression>{state.state()};
+	//exprs += vector<smtutil::Expression>{state.state()};
 	exprs += _contract ? newStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->increaseIndex(); });
 	exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp
index dc134766d..4ce9e57ed 100644
--- a/libsolidity/formal/PredicateSort.cpp
+++ b/libsolidity/formal/PredicateSort.cpp
@@ -31,7 +31,7 @@ namespace solidity::frontend::smt
 SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
 {
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
+		vector<SortPointer>{_state.thisAddressSort()/*, _state.abiSort(), _state.cryptoSort(), _state.stateSort()*/} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }
@@ -39,12 +39,12 @@ SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _s
 SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
 {
 	auto varSorts = stateSorts(_contract);
-	vector<SortPointer> stateSort{_state.stateSort()};
+	//vector<SortPointer> stateSort{_state.stateSort()};
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
-			stateSort +
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort()/*, _state.abiSort(), _state.cryptoSort()*/} +
+			//stateSort +
 			varSorts +
-			stateSort +
+			//stateSort +
 			varSorts,
 		SortProvider::boolSort
 	);
@@ -56,9 +56,9 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
 		return functionSort(*constructor, &_contract, _state);
 
 	auto varSorts = stateSorts(_contract);
-	vector<SortPointer> stateSort{_state.stateSort()};
+	//vector<SortPointer> stateSort{_state.stateSort()};
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort()/*, _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()*/} + varSorts + varSorts,
 		SortProvider::boolSort
 	);
 }
@@ -70,10 +70,10 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort()/*, _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()*/} +
 			varSorts +
 			inputSorts +
-			vector<SortPointer>{_state.stateSort()} +
+			//vector<SortPointer>{_state.stateSort()} +
 			varSorts +
 			inputSorts +
 			outputSorts,
diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp
index 582cb3739..1bde68b10 100644
--- a/libsolidity/formal/SymbolicState.cpp
+++ b/libsolidity/formal/SymbolicState.cpp
@@ -75,13 +75,13 @@ void SymbolicState::reset()
 {
 	m_error.resetIndex();
 	m_thisAddress.resetIndex();
-	m_state.reset();
-	m_tx.reset();
-	m_crypto.reset();
+	//m_state.reset();
+	//m_tx.reset();
+	//m_crypto.reset();
 	/// We don't reset m_abi's pointer nor clear m_abiMembers on purpose,
 	/// since it only helps to keep the already generated types.
-	solAssert(m_abi, "");
-	m_abi->reset();
+	//solAssert(m_abi, "");
+	//m_abi->reset();
 }
 
 smtutil::Expression SymbolicState::balances() const
@@ -128,6 +128,8 @@ smtutil::Expression SymbolicState::txMember(string const& _member) const
 
 smtutil::Expression SymbolicState::txTypeConstraints() const
 {
+	return smtutil::Expression(true);
+
 	return smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::address()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.difficulty"), TypeProvider::uint256()) &&
@@ -142,11 +144,14 @@ smtutil::Expression SymbolicState::txTypeConstraints() const
 
 smtutil::Expression SymbolicState::txNonPayableConstraint() const
 {
+	return smtutil::Expression(true);
 	return m_tx.member("msg.value") == 0;
 }
 
 smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition const& _function) const
 {
+	return smtutil::Expression(true);
+
 	smtutil::Expression conj = _function.isPayable() ? smtutil::Expression(true) : txNonPayableConstraint();
 	if (_function.isPartOfExternalInterface())
 	{
@@ -169,12 +174,14 @@ smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition cons
 	return conj;
 }
 
-void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
+void SymbolicState::prepareForSourceUnit(SourceUnit const& /*_source*/)
 {
+	/*
 	set<FunctionCall const*> abiCalls = SMTEncoder::collectABICalls(&_source);
 	for (auto const& source: _source.referencedSourceUnits(true))
 		abiCalls += SMTEncoder::collectABICalls(source);
 	buildABIFunctions(abiCalls);
+	*/
 }
 
 /// Private helpers.
diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol
index b8727aab4..c0bb305b9 100644
--- a/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol
@@ -24,7 +24,7 @@ contract C {
 	// Fails due to j.
 	function i() public view {
 		// Disabled because Spacer 4.8.9 seg faults.
-		//assert(x < 2);
+		assert(x < 2);
 	}
 }
 // ====