Merge pull request #13883 from ethereum/default-evmversion-paris

Set default EVM version to Paris

.circleci/soltest_all.sh

@@ -32,7 +32,7 @@ REPODIR="$(realpath "$(dirname "$0")"/..)"
 source "${REPODIR}/scripts/common.sh"
 
 EVM_VALUES=(homestead byzantium constantinople petersburg istanbul berlin london paris)
-DEFAULT_EVM=london
+DEFAULT_EVM=paris
 [[ " ${EVM_VALUES[*]} " =~ $DEFAULT_EVM ]]
 OPTIMIZE_VALUES=(0 1)
 

Changelog.md

@@ -9,6 +9,7 @@ Compiler Features:
  * Commandline Interface: Add `--no-cbor-metadata` that skips CBOR metadata from getting appended at the end of the bytecode.
  * EVM: Deprecate ``block.difficulty`` and disallow ``difficulty()`` in inline assembly for EVM versions >= paris. The change is due to the renaming introduced by [EIP-4399](https://eips.ethereum.org/EIPS/eip-4399).
  * EVM: Introduce ``block.prevrandao`` in Solidity and ``prevrandao()`` in inline assembly for EVM versions >= paris.
+ * EVM: Set the default EVM version to "Paris".
  * EVM: Support for the EVM version "Paris".
  * Natspec: Add event Natspec inheritance for devdoc.
  * Standard JSON: Add a boolean field `settings.metadata.appendCBOR` that skips CBOR metadata from getting appended at the end of the bytecode.

docs/using-the-compiler.rst

@@ -170,10 +170,10 @@ at each version. Backward compatibility is not guaranteed between each version.
    - Gas costs for ``SLOAD``, ``*CALL``, ``BALANCE``, ``EXT*`` and ``SELFDESTRUCT`` increased. The
      compiler assumes cold gas costs for such operations. This is relevant for gas estimation and
      the optimizer.
-- ``london`` (**default**)
+- ``london``
    - The block's base fee (`EIP-3198 <https://eips.ethereum.org/EIPS/eip-3198>`_ and `EIP-1559 <https://eips.ethereum.org/EIPS/eip-1559>`_) can be accessed via the global ``block.basefee`` or ``basefee()`` in inline assembly.
-- ``paris``
+- ``paris`` (**default**)
-   - No changes, however the semantics of the ``difficulty`` value have changed (see `EIP-4399 <https://eips.ethereum.org/EIPS/eip-4399>`_).
+   - Introduces ``prevrandao()`` and ``block.prevrandao``, and changes the semantics of the now deprecated ``block.difficulty``, disallowing ``difficulty()`` in inline assembly (see `EIP-4399 <https://eips.ethereum.org/EIPS/eip-4399>`_).
 
 .. index:: ! standard JSON, ! --standard-json
 .. _compiler-api:

liblangutil/EVMVersion.h

@@ -109,7 +109,7 @@ private:
 
 	EVMVersion(Version _version): m_version(_version) {}
 
-	Version m_version = Version::London;
+	Version m_version = Version::Paris;
 };
 
 }

libsolidity/formal/Predicate.cpp

@@ -255,8 +255,14 @@ string Predicate::formatSummaryCall(
 					if (auto const* identifier = dynamic_cast<Identifier const*>(memberExpr))
 					{
 						ASTString const& name = identifier->name();
+						auto memberName = _memberAccess.memberName();
+
+						// TODO remove this for 0.9.0
+						if (name == "block" && memberName == "difficulty")
+							memberName = "prevrandao";
+
 						if (name == "block" || name == "msg" || name == "tx")
-							txVars.insert(name + "." + _memberAccess.memberName());
+							txVars.insert(name + "." + memberName);
 					}
 
 				return true;
@@ -642,7 +648,7 @@ map<string, optional<string>> Predicate::readTxVars(smtutil::Expression const& _
 		{"block.basefee", TypeProvider::uint256()},
 		{"block.chainid", TypeProvider::uint256()},
 		{"block.coinbase", TypeProvider::address()},
-		{"block.difficulty", TypeProvider::uint256()},
+		{"block.prevrandao", TypeProvider::uint256()},
 		{"block.gaslimit", TypeProvider::uint256()},
 		{"block.number", TypeProvider::uint256()},
 		{"block.timestamp", TypeProvider::uint256()},

libsolidity/formal/SMTEncoder.cpp

@@ -1337,7 +1337,13 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		{
 			auto const& name = identifier->name();
 			solAssert(name == "block" || name == "msg" || name == "tx", "");
-			defineExpr(_memberAccess, state().txMember(name + "." + _memberAccess.memberName()));
+			auto memberName = _memberAccess.memberName();
+
+			// TODO remove this for 0.9.0
+			if (name == "block" && memberName == "difficulty")
+				memberName = "prevrandao";
+
+			defineExpr(_memberAccess, state().txMember(name + "." + memberName));
 		}
 		else if (auto magicType = dynamic_cast<MagicType const*>(exprType))
 		{

libsolidity/formal/SymbolicState.cpp

@@ -142,13 +142,20 @@ smtutil::Expression SymbolicState::txMember(string const& _member) const
 	return m_tx.member(_member);
 }
 
+smtutil::Expression SymbolicState::evmParisConstraints() const
+{
+	// Ensure prevrandao range as defined by EIP-4399.
+	return txMember("block.prevrandao") > (u256(1) << 64);
+}
+
 smtutil::Expression SymbolicState::txTypeConstraints() const
 {
 	return
+		evmParisConstraints() &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.basefee"), TypeProvider::uint256()) &&
 		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()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("block.prevrandao"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.gaslimit"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.number"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.timestamp"), TypeProvider::uint256()) &&

libsolidity/formal/SymbolicState.h

@@ -68,9 +68,9 @@ private:
  *   - block basefee
  *   - block chainid
  *   - block coinbase
- *   - block difficulty
  *   - block gaslimit
  *   - block number
+ *   - block prevrandao
  *   - block timestamp
  *   - TODO gasleft
  *   - msg data
@@ -136,6 +136,7 @@ public:
 	smtutil::Expression txTypeConstraints() const;
 	smtutil::Expression txNonPayableConstraint() const;
 	smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
+	smtutil::Expression evmParisConstraints() const;
 	//@}
 
 	/// Crypto functions.
@@ -197,7 +198,7 @@ private:
 			{"block.basefee", smtutil::SortProvider::uintSort},
 			{"block.chainid", smtutil::SortProvider::uintSort},
 			{"block.coinbase", smt::smtSort(*TypeProvider::address())},
-			{"block.difficulty", smtutil::SortProvider::uintSort},
+			{"block.prevrandao", smtutil::SortProvider::uintSort},
 			{"block.gaslimit", smtutil::SortProvider::uintSort},
 			{"block.number", smtutil::SortProvider::uintSort},
 			{"block.timestamp", smtutil::SortProvider::uintSort},

scripts/tests.sh

@@ -115,9 +115,9 @@ do
     for vm in $EVM_VERSIONS
     do
         FORCE_ABIV1_RUNS="no"
-        if [[ "$vm" == "london" ]]
+        if [[ "$vm" == "paris" ]]
         then
-            FORCE_ABIV1_RUNS="no yes" # run both in london
+            FORCE_ABIV1_RUNS="no yes" # run both in paris
         fi
         for abiv1 in $FORCE_ABIV1_RUNS
         do

test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json

@@ -3,38 +3,11 @@
     {
         "smtlib2queries":
         {
-            "0x2bcd3328dc8d31e869efd5e0dfdb16a6fa26f0a9c2829ea55670262be485e401": "(set-option :produce-models true)
+            "0x0ebc730de380833af1e52ed063befb32994bc637929c942b7fd089b7cd3ba64e": "(set-logic HORN)
-(set-logic ALL)
-(declare-fun |x_3_3| () Int)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
-(declare-fun |abi_0| () |abi_type|)
-(declare-fun |x_3_4| () Int)
-(declare-fun |x_3_0| () Int)
-(declare-fun |expr_7_0| () Int)
-(declare-fun |expr_8_0| () Int)
-(declare-fun |expr_9_1| () Bool)
-
-(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
-(declare-const |EVALEXPR_0| Int)
-(assert (= |EVALEXPR_0| x_3_0))
-(check-sat)
-(get-value (|EVALEXPR_0| ))
-",
-            "0x4e70784a8a93c7429a716aa8b778f3de5d1f63b30158452534da5d44e5967d2b": "(set-logic HORN)
 
 (declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
 (declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
 (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
 (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
 (declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
@@ -95,7 +68,7 @@
 
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> (and (and (block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 x_3_1 state_3 x_3_2) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true))))))) true) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_3 x_3_2))))
+(=> (and (and (block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 x_3_1 state_3 x_3_2) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true))))))) true) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_3 x_3_2))))
 
 
 (assert
@@ -139,7 +112,7 @@
 
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> (and (and (summary_constructor_2_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
+(=> (and (and (summary_constructor_2_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
 
 
 (declare-fun |error_target_3_0| () Bool)
@@ -151,7 +124,34 @@
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
 (=> error_target_3_0 false)))
-(check-sat)"
+(check-sat)",
+            "0xcb822e6220a39244d26887a0fa6f62b06718359056555679fb06dd7dff18bb86": "(set-option :produce-models true)
+(set-logic ALL)
+(declare-fun |x_3_3| () Int)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
+(declare-fun |abi_0| () |abi_type|)
+(declare-fun |x_3_4| () Int)
+(declare-fun |x_3_0| () Int)
+(declare-fun |expr_7_0| () Int)
+(declare-fun |expr_8_0| () Int)
+(declare-fun |expr_9_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| x_3_0))
+(check-sat)
+(get-value (|EVALEXPR_0| ))
+"
         }
     },
     "errors":

test/externalTests/common.sh

@@ -22,7 +22,7 @@ set -e
 
 # Requires $REPO_ROOT to be defined and "${REPO_ROOT}/scripts/common.sh" to be included before.
 
-CURRENT_EVM_VERSION=london
+CURRENT_EVM_VERSION=paris
 
 AVAILABLE_PRESETS=(
     legacy-no-optimize

test/libsolidity/StandardCompiler.cpp

@@ -1086,7 +1086,7 @@ BOOST_AUTO_TEST_CASE(evm_version)
 	BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"paris\"") != string::npos);
 	// test default
 	result = compile(inputForVersion(""));
-	BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"london\"") != string::npos);
+	BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"paris\"") != string::npos);
 	// test invalid
 	result = compile(inputForVersion("\"evmVersion\": \"invalid\","));
 	BOOST_CHECK(result["errors"][0]["message"].asString() == "Invalid EVM version requested.");

test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol

@@ -3,12 +3,13 @@ contract C {
 		bytes memory b1 = abi.encodeWithSignature(sig, x, a);
 		bytes memory b2 = abi.encodeWithSelector(bytes4(keccak256(bytes(sig))), x, a);
 		// should hold but we do not evaluate keccak256 in an interpreted way
-		assert(b1.length == b2.length);
+		//assert(b1.length == b2.length);
+		assert(b1.length != b2.length); // should fail
 	}
 }
 // ====
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (294-324): CHC: Assertion violation might happen here.
+// Warning 6328: (330-360): CHC: Assertion violation might happen here.
-// Warning 7812: (294-324): BMC: Assertion violation might happen here.
+// Warning 7812: (330-360): BMC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol

@@ -26,7 +26,7 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (335-365): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [69]\nb2 = [0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(sig, [69])
+// Warning 6328: (335-365): CHC: Assertion violation happens here.
 // Warning 6328: (589-619): CHC: Assertion violation happens here.
 // Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
 // Warning 4661: (1087-1117): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/bmc_coverage/range_check.sol

@@ -17,6 +17,8 @@ contract C {
 		assert(block.chainid <= 2**256 - 1);
 		assert(block.difficulty >= 0);
 		assert(block.difficulty <= 2**256 - 1);
+		assert(block.prevrandao > 2**64);
+		assert(block.prevrandao <= 2**256 - 1);
 		assert(block.gaslimit >= 0);
 		assert(block.gaslimit <= 2**256 - 1);
 		assert(block.number >= 0);
@@ -44,6 +46,8 @@ contract D {
 			assert(block.chainid <= 2**256 - 1);
 			assert(block.difficulty >= 0);
 			assert(block.difficulty <= 2**256 - 1);
+			assert(block.prevrandao > 2**64);
+			assert(block.prevrandao <= 2**256 - 1);
 			assert(block.gaslimit >= 0);
 			assert(block.gaslimit <= 2**256 - 1);
 			assert(block.number >= 0);
@@ -54,3 +58,7 @@ contract D {
 // ====
 // SMTEngine: bmc
 // ----
+// Warning 8417: (565-581): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (598-614): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (1447-1463): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (1481-1497): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.

test/libsolidity/smtCheckerTests/external_calls/external_safe.sol

@@ -16,5 +16,5 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
-// Info 1180: Contract invariant(s) for :C:\n!(x >= 11)\nReentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!(x <= 10) || !(<errorCode> >= 3)) && (!(x <= 10) || !(x' >= 11)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Overflow at ++x\n<errorCode> = 3 -> Assertion failed at assert(x < 11)\n

test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol

@@ -30,7 +30,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTSolvers: z3
 // SMTIgnoreOS: macos
+// SMTSolvers: z3
 // ----
-// Info 1180: Contract invariant(s) for :C:\n!(x >= 7)\n

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol

@@ -24,6 +24,6 @@ contract LoopFor2 {
 }
 // ====
 // SMTEngine: all
-// SMTSolvers: z3
 // SMTIgnoreOS: macos
+// SMTSolvers: z3
 // ----

test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol

@@ -6,5 +6,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6368: (76-90): CHC: Out of bounds access might happen here.

test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol

@@ -22,6 +22,6 @@ contract C {
 // ----
 // Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here.
-// Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r()
+// Warning 6368: (259-263): CHC: Out of bounds access happens here.
 // Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here.

test/libsolidity/smtCheckerTests/special/block_vars_bmc_internal.sol

@@ -1,12 +1,14 @@
 contract C {
 	address coin;
 	uint dif;
+	uint prevrandao;
 	uint gas;
 	uint number;
 	uint timestamp;
 	function f() public {
 		coin = block.coinbase;
 		dif = block.difficulty;
+		prevrandao = block.prevrandao;
 		gas = block.gaslimit;
 		number = block.number;
 		timestamp = block.timestamp;
@@ -16,12 +18,14 @@ contract C {
 	function g() internal view {
 		assert(uint160(coin) >= 0); // should hold
 		assert(dif >= 0); // should hold
+		assert(prevrandao > 2**64); // should hold
 		assert(gas >= 0); // should hold
 		assert(number >= 0); // should hold
 		assert(timestamp >= 0); // should hold
 
 		assert(coin == block.coinbase); // should fail with BMC
 		assert(dif == block.difficulty); // should fail with BMC
+		assert(prevrandao == block.prevrandao); // should fail with BMC
 		assert(gas == block.gaslimit); // should fail with BMC
 		assert(number == block.number); // should fail with BMC
 		assert(timestamp == block.timestamp); // should fail with BMC
@@ -30,8 +34,12 @@ contract C {
 // ====
 // SMTEngine: bmc
 // ----
-// Warning 4661: (473-503): BMC: Assertion violation happens here.
+// Warning 8417: (155-171): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
-// Warning 4661: (531-562): BMC: Assertion violation happens here.
+// Warning 8417: (641-657): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
-// Warning 4661: (590-619): BMC: Assertion violation happens here.
+// Warning 4661: (409-435): BMC: Assertion violation happens here.
-// Warning 4661: (647-677): BMC: Assertion violation happens here.
+// Warning 4661: (569-599): BMC: Assertion violation happens here.
-// Warning 4661: (705-741): BMC: Assertion violation happens here.
+// Warning 4661: (627-658): BMC: Assertion violation happens here.
+// Warning 4661: (686-724): BMC: Assertion violation happens here.
+// Warning 4661: (752-781): BMC: Assertion violation happens here.
+// Warning 4661: (809-839): BMC: Assertion violation happens here.
+// Warning 4661: (867-903): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol

@@ -1,12 +1,14 @@
 contract C {
 	address coin;
 	uint dif;
+	uint prevrandao;
 	uint gas;
 	uint number;
 	uint timestamp;
 	function f() public {
 		coin = block.coinbase;
 		dif = block.difficulty;
+		prevrandao = block.prevrandao;
 		gas = block.gaslimit;
 		number = block.number;
 		timestamp = block.timestamp;
@@ -16,12 +18,14 @@ contract C {
 	function g() internal view {
 		assert(uint160(coin) >= 0); // should hold
 		assert(dif >= 0); // should hold
+		assert(prevrandao > 2**64); // should hold
 		assert(gas >= 0); // should hold
 		assert(number >= 0); // should hold
 		assert(timestamp >= 0); // should hold
 
 		assert(coin == block.coinbase); // should hold with CHC
 		assert(dif == block.difficulty); // should hold with CHC
+		assert(prevrandao == block.prevrandao); // should hold with CHC
 		assert(gas == block.gaslimit); // should hold with CHC
 		assert(number == block.number); // should hold with CHC
 		assert(timestamp == block.timestamp); // should hold with CHC
@@ -33,4 +37,6 @@ contract C {
 // SMTEngine: chc
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n    C.g() -- internal call
+// Warning 8417: (155-171): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (641-657): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 6328: (932-961): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/difficulty.sol

@@ -1,11 +0,0 @@
-contract C
-{
-	function f(uint difficulty) public view {
-		assert(block.difficulty == difficulty);
-	}
-}
-// ====
-// SMTEngine: all
-// SMTIgnoreCex: yes
-// ----
-// Warning 6328: (58-96): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/many.sol

@@ -3,6 +3,7 @@ contract C
 	function f() public payable {
 		assert(msg.sender == block.coinbase);
 		assert(block.difficulty == block.gaslimit);
+		assert(block.prevrandao == block.gaslimit);
 		assert(block.number == block.timestamp);
 		assert(tx.gasprice == msg.value);
 		assert(tx.origin == msg.sender);
@@ -17,11 +18,13 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 8417: (93-109): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
 // Warning 6328: (46-82): CHC: Assertion violation happens here.
 // Warning 6328: (86-128): CHC: Assertion violation happens here.
-// Warning 6328: (132-171): CHC: Assertion violation happens here.
+// Warning 6328: (132-174): CHC: Assertion violation happens here.
-// Warning 6328: (175-207): CHC: Assertion violation happens here.
+// Warning 6328: (178-217): CHC: Assertion violation happens here.
-// Warning 6328: (211-242): CHC: Assertion violation happens here.
+// Warning 6328: (221-253): CHC: Assertion violation happens here.
-// Warning 6328: (295-319): CHC: Assertion violation happens here.
+// Warning 6328: (257-288): CHC: Assertion violation happens here.
-// Warning 6328: (323-351): CHC: Assertion violation happens here.
+// Warning 6328: (341-365): CHC: Assertion violation happens here.
-// Warning 6328: (355-378): CHC: Assertion violation happens here.
+// Warning 6328: (369-397): CHC: Assertion violation happens here.
+// Warning 6328: (401-424): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/many_internal.sol

@@ -6,6 +6,7 @@ contract C
 	function g() internal {
 		assert(msg.sender == block.coinbase);
 		assert(block.difficulty == block.gaslimit);
+		assert(block.prevrandao == block.gaslimit);
 		assert(block.number == block.timestamp);
 		assert(tx.gasprice == msg.value);
 		assert(tx.origin == msg.sender);
@@ -20,11 +21,13 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 8417: (128-144): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
 // Warning 6328: (81-117): CHC: Assertion violation happens here.
 // Warning 6328: (121-163): CHC: Assertion violation happens here.
-// Warning 6328: (167-206): CHC: Assertion violation happens here.
+// Warning 6328: (167-209): CHC: Assertion violation happens here.
-// Warning 6328: (210-242): CHC: Assertion violation happens here.
+// Warning 6328: (213-252): CHC: Assertion violation happens here.
-// Warning 6328: (246-277): CHC: Assertion violation happens here.
+// Warning 6328: (256-288): CHC: Assertion violation happens here.
-// Warning 6328: (330-354): CHC: Assertion violation happens here.
+// Warning 6328: (292-323): CHC: Assertion violation happens here.
-// Warning 6328: (358-386): CHC: Assertion violation happens here.
+// Warning 6328: (376-400): CHC: Assertion violation happens here.
-// Warning 6328: (390-413): CHC: Assertion violation happens here.
+// Warning 6328: (404-432): CHC: Assertion violation happens here.
+// Warning 6328: (436-459): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/prevrandao.sol

@@ -0,0 +1,16 @@
+contract C
+{
+	function f(uint prevrandao) public view {
+		assert(block.prevrandao == prevrandao); // should fail
+		assert(block.difficulty == prevrandao); // should fail
+		assert(block.difficulty == block.prevrandao); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 8417: (122-138): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (179-195): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 6328: (58-96): CHC: Assertion violation happens here.
+// Warning 6328: (115-153): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/range_check.sol

@@ -17,6 +17,8 @@ contract C {
 		assert(block.chainid <= 2**256 - 1);
 		assert(block.difficulty >= 0);
 		assert(block.difficulty <= 2**256 - 1);
+		assert(block.prevrandao > 2**64);
+		assert(block.prevrandao <= 2**256 - 1);
 		assert(block.gaslimit >= 0);
 		assert(block.gaslimit <= 2**256 - 1);
 		assert(block.number >= 0);
@@ -44,6 +46,8 @@ contract D {
 			assert(block.chainid <= 2**256 - 1);
 			assert(block.difficulty >= 0);
 			assert(block.difficulty <= 2**256 - 1);
+			assert(block.prevrandao > 2**64);
+			assert(block.prevrandao <= 2**256 - 1);
 			assert(block.gaslimit >= 0);
 			assert(block.gaslimit <= 2**256 - 1);
 			assert(block.number >= 0);
@@ -55,3 +59,7 @@ contract D {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8417: (565-581): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (598-614): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (1447-1463): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (1481-1497): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.

test/libsolidity/smtCheckerTests/special/tx_data_immutable.sol

@@ -2,6 +2,7 @@ contract C {
 	bytes32 bhash;
 	address coin;
 	uint dif;
+	uint prevrandao;
 	uint glimit;
 	uint number;
 	uint tstamp;
@@ -16,6 +17,7 @@ contract C {
 		bhash = blockhash(12);
 		coin = block.coinbase;
 		dif = block.difficulty;
+		prevrandao = block.prevrandao;
 		glimit = block.gaslimit;
 		number = block.number;
 		tstamp = block.timestamp;
@@ -31,6 +33,7 @@ contract C {
 		assert(bhash == blockhash(12));
 		assert(coin == block.coinbase);
 		assert(dif == block.difficulty);
+		assert(prevrandao == block.prevrandao);
 		assert(glimit == block.gaslimit);
 		assert(number == block.number);
 		assert(tstamp == block.timestamp);
@@ -46,6 +49,7 @@ contract C {
 		assert(bhash == blockhash(12));
 		assert(coin == block.coinbase);
 		assert(dif == block.difficulty);
+		assert(prevrandao == block.prevrandao);
 		assert(glimit == block.gaslimit);
 		assert(number == block.number);
 		assert(tstamp == block.timestamp);
@@ -60,3 +64,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8417: (293-309): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (645-661): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
+// Warning 8417: (1127-1143): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.

test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol

@@ -2,6 +2,7 @@ contract C {
 	bytes32 bhash;
 	address coin;
 	uint dif;
+	uint prevrandao;
 	uint glimit;
 	uint number;
 	uint tstamp;
@@ -16,6 +17,7 @@ contract C {
 		bhash = blockhash(12);
 		coin = block.coinbase;
 		dif = block.difficulty;
+		prevrandao = block.prevrandao;
 		glimit = block.gaslimit;
 		number = block.number;
 		tstamp = block.timestamp;
@@ -31,6 +33,7 @@ contract C {
 		assert(bhash == blockhash(122));
 		assert(coin != block.coinbase);
 		assert(dif != block.difficulty);
+		assert(prevrandao != block.prevrandao);
 		assert(glimit != block.gaslimit);
 		assert(number != block.number);
 		assert(tstamp != block.timestamp);
@@ -46,6 +49,7 @@ contract C {
 		assert(bhash == blockhash(122));
 		assert(coin != block.coinbase);
 		assert(dif != block.difficulty);
+		assert(prevrandao != block.prevrandao);
 		assert(glimit != block.gaslimit);
 		assert(number != block.number);
 		assert(tstamp != block.timestamp);
@@ -61,27 +65,32 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (512-543): CHC: Assertion violation happens here.
+// Warning 8417: (293-309): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
-// Warning 6328: (547-577): CHC: Assertion violation happens here.
+// Warning 8417: (646-662): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
-// Warning 6328: (581-612): CHC: Assertion violation happens here.
+// Warning 8417: (1129-1145): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
-// Warning 6328: (616-648): CHC: Assertion violation happens here.
+// Warning 6328: (563-594): CHC: Assertion violation happens here.
-// Warning 6328: (652-682): CHC: Assertion violation happens here.
+// Warning 6328: (598-628): CHC: Assertion violation happens here.
-// Warning 6328: (686-719): CHC: Assertion violation happens here.
+// Warning 6328: (632-663): CHC: Assertion violation happens here.
-// Warning 6328: (723-762): CHC: Assertion violation happens here.
+// Warning 6328: (667-705): CHC: Assertion violation happens here.
-// Warning 6328: (766-794): CHC: Assertion violation happens here.
+// Warning 6328: (709-741): CHC: Assertion violation happens here.
-// Warning 6328: (798-820): CHC: Assertion violation happens here.
+// Warning 6328: (745-775): CHC: Assertion violation happens here.
-// Warning 6328: (824-850): CHC: Assertion violation happens here.
+// Warning 6328: (779-812): CHC: Assertion violation happens here.
-// Warning 6328: (854-883): CHC: Assertion violation happens here.
+// Warning 6328: (816-855): CHC: Assertion violation happens here.
-// Warning 6328: (887-914): CHC: Assertion violation happens here.
+// Warning 6328: (859-887): CHC: Assertion violation happens here.
-// Warning 6328: (953-984): CHC: Assertion violation happens here.
+// Warning 6328: (891-913): CHC: Assertion violation happens here.
-// Warning 6328: (988-1018): CHC: Assertion violation happens here.
+// Warning 6328: (917-943): CHC: Assertion violation happens here.
-// Warning 6328: (1022-1053): CHC: Assertion violation happens here.
+// Warning 6328: (947-976): CHC: Assertion violation happens here.
-// Warning 6328: (1057-1089): CHC: Assertion violation happens here.
+// Warning 6328: (980-1007): CHC: Assertion violation happens here.
-// Warning 6328: (1093-1123): CHC: Assertion violation happens here.
+// Warning 6328: (1046-1077): CHC: Assertion violation happens here.
-// Warning 6328: (1127-1160): CHC: Assertion violation happens here.
+// Warning 6328: (1081-1111): CHC: Assertion violation happens here.
-// Warning 6328: (1164-1203): CHC: Assertion violation happens here.
+// Warning 6328: (1115-1146): CHC: Assertion violation happens here.
-// Warning 6328: (1207-1235): CHC: Assertion violation happens here.
+// Warning 6328: (1150-1188): CHC: Assertion violation happens here.
-// Warning 6328: (1239-1261): CHC: Assertion violation happens here.
+// Warning 6328: (1192-1224): CHC: Assertion violation happens here.
-// Warning 6328: (1265-1291): CHC: Assertion violation happens here.
+// Warning 6328: (1228-1258): CHC: Assertion violation happens here.
-// Warning 6328: (1295-1324): CHC: Assertion violation happens here.
+// Warning 6328: (1262-1295): CHC: Assertion violation happens here.
-// Warning 6328: (1328-1355): CHC: Assertion violation happens here.
+// Warning 6328: (1299-1338): CHC: Assertion violation happens here.
+// Warning 6328: (1342-1370): CHC: Assertion violation happens here.
+// Warning 6328: (1374-1396): CHC: Assertion violation happens here.
+// Warning 6328: (1400-1426): CHC: Assertion violation happens here.
+// Warning 6328: (1430-1459): CHC: Assertion violation happens here.
+// Warning 6328: (1463-1490): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol

@@ -32,5 +32,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
+// Warning 6368: (374-381): CHC: Out of bounds access might happen here.
 // Warning 6368: (456-462): CHC: Out of bounds access happens here.
-// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n!(a[2].length <= 2)\n

test/libsolidity/smtCheckerTests/userTypes/user_type_as_array_elem_1.sol

@@ -11,6 +11,8 @@ contract C {
         assert(T.unwrap(arr[i]) == address(42)); // should hold
     }
 }
+// ====
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (204-243): CHC: Assertion violation might happen here.
 // Warning 4661: (204-243): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/userTypes/user_type_as_struct_member_1.sol

@@ -23,3 +23,4 @@ contract C {
         );
     }
 }
+// ----