From 8fceb90a693c484b63edafcc4571a61987827ad4 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 23 Jan 2025 20:44:42 +0800 Subject: [PATCH] give sort to the generated var --- pyk/src/tests/integration/proof/test_refute_node.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index 34f99d4977..7c88732268 100644 --- a/pyk/src/tests/integration/proof/test_refute_node.py +++ b/pyk/src/tests/integration/proof/test_refute_node.py @@ -295,7 +295,7 @@ def test_apr_proof_refute_node_to_claim( expected = KClaim( body=KRewrite(KApply('_<=Int_', KVariable('N', 'Int'), KToken('0', 'Int')), KToken('false', 'Bool')), requires=KApply( - '_<=Int_', KApply('_+Int_', KVariable('_L', None), KVariable('N', 'Int')), KToken('0', 'Int') + '_<=Int_', KApply('_+Int_', KVariable('_L', 'Int'), KVariable('N', 'Int')), KToken('0', 'Int') ), att=KAtt(entries=[Atts.LABEL('refute-node-claim')]), )