From 5409bd40aba73d82201822f38c18dacfbe09deee Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 24 Nov 2023 17:08:47 +0100 Subject: [PATCH] Using builtin equals for definitions --- src/main/scala/supporters/functions/FunctionData.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala index 7e0b3cab2..98958fc71 100644 --- a/src/main/scala/supporters/functions/FunctionData.scala +++ b/src/main/scala/supporters/functions/FunctionData.scala @@ -73,7 +73,7 @@ class FunctionData(val programFunction: ast.Function, val limitedAxiom = Forall(arguments, - limitedFunctionApplication === functionApplication, + BuiltinEquals(limitedFunctionApplication, functionApplication), Trigger(functionApplication)) val triggerAxiom = @@ -258,7 +258,7 @@ class FunctionData(val programFunction: ast.Function, optBody.map(translatedBody => { val pre = preconditionFunctionApplication val nestedDefinitionalAxioms = generateNestedDefinitionalAxioms - val body = And(nestedDefinitionalAxioms ++ List(Implies(pre, And(functionApplication === translatedBody)))) + val body = And(nestedDefinitionalAxioms ++ List(Implies(pre, And(BuiltinEquals(functionApplication, translatedBody))))) val allTriggers = ( Seq(Trigger(functionApplication)) ++ predicateTriggers.values.map(pt => Trigger(Seq(triggerFunctionApplication, pt))))