diff --git a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
index 60f83c038..63a21eb4e 100644
--- a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
+++ b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
@@ -1,4 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x4ca2adc24a17cd524cf3113f3b2cddff216f428f804e884cf76d27dd3e72cd68":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x8b2c3058077c75f8fff85d2d387198b91b4e591448624f4bef0ab6c7b87d5ec1":"(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -7,6 +7,9 @@
 (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.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-fun |x_4_0| () Int)
 (declare-fun |expr_8_0| () Int)
 (declare-fun |expr_9_0| () Int)