Merge pull request viperproject#778 from viperproject/meilers_fix_777

Using builtin equals for definitions
viper-admin · Nov 24, 2023 · 37fbe36 · 37fbe36
2 parents 8fa723a + 525893c
commit 37fbe36
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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 funcAnn = programFunction.info.getUniqueInfo[ast.AnnotationInfo]
       val actualPredicateTriggers = funcAnn match {
         case Some(a) if a.values.contains("opaque") => Seq()