From 16c0299e1f22b517968e89020eecb67c613fa2f2 Mon Sep 17 00:00:00 2001
From: Marco Eilers <marco.eilers@inf.ethz.ch>
Date: Tue, 23 Jul 2019 18:44:27 +0200
Subject: [PATCH 1/5] Backend support for SMTLib types (particularly bitvectors
 and floats)

---
 .../scala/viper/silver/ast/Expression.scala   | 12 +++
 src/main/scala/viper/silver/ast/Program.scala |  4 +
 src/main/scala/viper/silver/ast/Type.scala    |  2 +
 .../silver/ast/pretty/PrettyPrinter.scala     |  3 +
 .../silver/ast/utility/Expressions.scala      |  1 +
 .../viper/silver/ast/utility/Nodes.scala      |  1 +
 .../silver/ast/utility/SMTTypeFactories.scala | 73 +++++++++++++++++++
 .../viper/silver/ast/utility/Types.scala      |  2 +-
 8 files changed, 97 insertions(+), 1 deletion(-)
 create mode 100644 src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 46b4e30e3..bf31051ef 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -387,6 +387,18 @@ object DomainFuncApp {
     DomainFuncApp(func.name,args,typVarMap)(pos, info, func.typ.substitute(typVarMap), func.domainName, errT)
 }
 
+// --- References to built-in SMT Lib functions
+
+case class SMTFuncApp(smtfunc: SMTFunc, args: Seq[Exp])
+                     (val pos: Position, val info: Info, override val typ : Type, val errT: ErrorTrafo)
+  extends AbstractDomainFuncApp with PossibleTrigger {
+  override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
+  def getArgs = args
+  def withArgs(newArgs: Seq[Exp]) = SMTFuncApp(smtfunc, newArgs)(pos,info,typ, errT)
+  override def func = (p: Program) => smtfunc
+  def funcname = smtfunc.name
+}
+
 // --- Field and predicate accesses
 
 /** A common trait for expressions accessing a location. */
diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index 6c8c8822e..32fe650b9 100644
--- a/src/main/scala/viper/silver/ast/Program.scala
+++ b/src/main/scala/viper/silver/ast/Program.scala
@@ -705,3 +705,7 @@ case object NotOp extends UnOp with BoolDomainFunc {
   lazy val priority = 10
   lazy val fixity = Prefix
 }
+
+
+case class SMTFunc(name: String, smtName: String, override val typ: Type, override val formalArgs: Seq[LocalVarDecl]) extends Node with AbstractDomainFunc with BuiltinDomainFunc
+
diff --git a/src/main/scala/viper/silver/ast/Type.scala b/src/main/scala/viper/silver/ast/Type.scala
index 0459ad752..69d265528 100644
--- a/src/main/scala/viper/silver/ast/Type.scala
+++ b/src/main/scala/viper/silver/ast/Type.scala
@@ -183,3 +183,5 @@ case class TypeVar(name: String) extends Type {
 
   //def !=(other: TypeVar) = name != other
 }
+
+case class SMTType(boogieName: String, smtName: String) extends AtomicType
diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
index ae5fbdde5..e9327793d 100644
--- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -618,6 +618,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       case dt@DomainType(domainName, typVarsMap) =>
         val typArgs = dt.typeParameters map (t => show(typVarsMap.getOrElse(t, t)))
         text(domainName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char (',') <> space)))
+      case SMTType(boogieName, _) => boogieName
     }
   }
 
@@ -766,6 +767,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       text(funcname) <> parens(ssep(args map show, char (',') <> space))
     case DomainFuncApp(funcname, args, _) =>
       text(funcname) <> parens(ssep(args map show, char (',') <> space))
+    case SMTFuncApp(func, args) =>
+      text(func.name) <> parens(ssep(args map show, char(',') <> space))
 
     case EmptySeq(elemTyp) =>
       text("Seq[") <> showType(elemTyp) <> "]()"
diff --git a/src/main/scala/viper/silver/ast/utility/Expressions.scala b/src/main/scala/viper/silver/ast/utility/Expressions.scala
index a276b3270..d7bd43b79 100644
--- a/src/main/scala/viper/silver/ast/utility/Expressions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Expressions.scala
@@ -32,6 +32,7 @@ object Expressions {
          | _: PermExp
          | _: FuncApp
          | _: DomainFuncApp
+         | _: SMTFuncApp
          | _: LocationAccess
          | _: AbstractLocalVar
          | _: SeqExp
diff --git a/src/main/scala/viper/silver/ast/utility/Nodes.scala b/src/main/scala/viper/silver/ast/utility/Nodes.scala
index a473e03fd..0fa71fff7 100644
--- a/src/main/scala/viper/silver/ast/utility/Nodes.scala
+++ b/src/main/scala/viper/silver/ast/utility/Nodes.scala
@@ -106,6 +106,7 @@ object Nodes {
           case FuncApp(_, args) => args
           case DomainFuncApp(_, args, m) =>
             args ++ m.keys ++ m.values
+          case SMTFuncApp(_, args) => args
 
           case EmptySeq(elemTyp) => Seq(elemTyp)
           case ExplicitSeq(elems) => elems
diff --git a/src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala b/src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala
new file mode 100644
index 000000000..368784240
--- /dev/null
+++ b/src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala
@@ -0,0 +1,73 @@
+package viper.silver.ast.utility
+
+import viper.silver.ast.{Bool, Int, LocalVarDecl, SMTFunc, SMTType}
+
+/**
+  * A factory for fixed-size bitvectors that offers convenient access to bitvector types, as well as
+  * function definitions for unary and binary functions on bitvectors, as well as conversions from and
+  * to integers.
+  */
+case class BVFactory(size: Int) {
+  lazy val typ = SMTType(s"bv${size}", s"(_ BitVec ${size})")
+
+  def xor(name: String) = SMTFunc(name, "bvxor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def and(name: String) = SMTFunc(name, "bvand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def or(name: String) = SMTFunc(name, "bvor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def add(name: String) = SMTFunc(name, "bvadd", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def mul(name: String) = SMTFunc(name, "bvmul", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def shl(name: String) = SMTFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def shr(name: String) = SMTFunc(name, "bvshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def not(name: String) = SMTFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)()))
+  def neg(name: String) = SMTFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)()))
+
+  def from_int(name: String) = SMTFunc(name, s"(_ int2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
+  def to_int(name: String) = SMTFunc(name, s"(_ bv2int ${size})", Int, Seq(LocalVarDecl("x", typ)()))
+  def from_nat(name: String) = SMTFunc(name, s"(_ nat2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
+  def to_nat(name: String) = SMTFunc(name, s"(_ bv2nat ${size})", Int, Seq(LocalVarDecl("x", typ)()))
+}
+
+/**
+  * Rounding modes for floating point operations.
+  */
+object RoundingMode extends Enumeration {
+  type RoundingMode = Value
+  val RNE, RNA, RTP, RTN, RTZ = Value
+}
+import RoundingMode._
+
+/**
+  * A factory for IEEE floating point numbers with "exp" bits for the exponent, "mant" bits for the significant,
+  * including the hidden bit, and a given rounding mode for all operations that use one.
+  * Offers access to types, unary and binary operations, comparisons, and conversions from and to
+  * bitvectors of size exp + mant.
+  */
+case class FloatFactory(mant: Int, exp: Int, roundingMode: RoundingMode) {
+
+  lazy val typ = SMTType(s"float${mant}e${exp}", s"(_ FloatingPoint ${exp} ${mant})")
+
+  def neg(name: String) = SMTFunc(name, "fp.neg", typ, Seq(LocalVarDecl("x", typ)()))
+  def abs(name: String) = SMTFunc(name, "fp.abs", typ, Seq(LocalVarDecl("x", typ)()))
+
+  def add(name: String) = SMTFunc(name, s"fp.add ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def sub(name: String) = SMTFunc(name, s"fp.sub ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def mul(name: String) = SMTFunc(name, s"fp.mul ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def div(name: String) = SMTFunc(name, s"fp.div ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def min(name: String) = SMTFunc(name, s"fp.min ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def max(name: String) = SMTFunc(name, s"fp.max ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def eq(name: String) = SMTFunc(name, s"fp.eq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def leq(name: String) = SMTFunc(name, s"fp.leq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def geq(name: String) = SMTFunc(name, s"fp.geq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def lt(name: String) = SMTFunc(name, s"fp.lt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def gt(name: String) = SMTFunc(name, s"fp.gt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def isZero(name: String) = SMTFunc(name, s"fp.isZero", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isInfinite(name: String) = SMTFunc(name, s"fp.isInfinite", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isNaN(name: String) = SMTFunc(name, s"fp.isNaN", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isNegative(name: String) = SMTFunc(name, s"fp.isNegative", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isPositive(name: String) = SMTFunc(name, s"fp.isPositive", Bool, Seq(LocalVarDecl("x", typ)()))
+
+  def from_bv(name: String) = SMTFunc(name, s"(_ to_fp ${exp} ${mant}) ", typ, Seq(LocalVarDecl("x", BVFactory(mant+exp).typ)()))
+  def to_bv(name: String) = SMTFunc(name, s"(_ fp.to_sbv ${exp+mant}) ${roundingMode} ", BVFactory(mant+exp).typ, Seq(LocalVarDecl("x", typ)()))
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/ast/utility/Types.scala b/src/main/scala/viper/silver/ast/utility/Types.scala
index b99c7c914..df754f5c0 100644
--- a/src/main/scala/viper/silver/ast/utility/Types.scala
+++ b/src/main/scala/viper/silver/ast/utility/Types.scala
@@ -69,7 +69,7 @@ object Types {
     * @return The list of transitive type constituents of `typ`.
     */
   def typeConstituents(typ: Type): List[Type] = typ match {
-    case Int | Bool | Perm | Ref | InternalType | _: TypeVar | Wand => Nil
+    case Int | Bool | Perm | Ref | InternalType | _: TypeVar | Wand | _: SMTType => Nil
     case dt: DomainType => dt.typeParameters.map(_.substitute(dt.typVarsMap)).toList
     case SeqType(elementType) => elementType :: typeConstituents(elementType)
     case SetType(elementType) => elementType :: typeConstituents(elementType)

From 071af4a412cd83c2dcccaeedd8a742b54ecf79aa Mon Sep 17 00:00:00 2001
From: Marco Eilers <marco.eilers@inf.ethz.ch>
Date: Mon, 29 Jul 2019 17:54:24 +0200
Subject: [PATCH 2/5] SMTFuncApps are no longer PossibleTriggers

---
 src/main/scala/viper/silver/ast/Expression.scala | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index bf31051ef..088ac50d2 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -391,10 +391,8 @@ object DomainFuncApp {
 
 case class SMTFuncApp(smtfunc: SMTFunc, args: Seq[Exp])
                      (val pos: Position, val info: Info, override val typ : Type, val errT: ErrorTrafo)
-  extends AbstractDomainFuncApp with PossibleTrigger {
+  extends AbstractDomainFuncApp {
   override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
-  def getArgs = args
-  def withArgs(newArgs: Seq[Exp]) = SMTFuncApp(smtfunc, newArgs)(pos,info,typ, errT)
   override def func = (p: Program) => smtfunc
   def funcname = smtfunc.name
 }

From 45adbede4a760f5abd2569f68439d69bfee9d6d4 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 24 Jul 2020 18:24:47 +0200
Subject: [PATCH 3/5] Added test for SMT types

---
 .../scala/viper/silver/ast/Expression.scala   |   9 +-
 src/main/scala/viper/silver/ast/Program.scala |   3 +-
 .../viper/silver/testing/SMTTypeTest.scala    | 165 ++++++++++++++++++
 3 files changed, 172 insertions(+), 5 deletions(-)
 create mode 100644 src/main/scala/viper/silver/testing/SMTTypeTest.scala

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index ba7ac248f..a1a5a754f 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -387,12 +387,13 @@ object DomainFuncApp {
 
 // --- References to built-in SMT Lib functions
 
-case class SMTFuncApp(smtfunc: SMTFunc, args: Seq[Exp])
-                     (val pos: Position, val info: Info, override val typ : Type, val errT: ErrorTrafo)
+case class SMTFuncApp(smtFunc: SMTFunc, args: Seq[Exp])
+                     (val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos)
   extends AbstractDomainFuncApp {
   override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
-  override def func = (p: Program) => smtfunc
-  def funcname = smtfunc.name
+  override def func = (p: Program) => smtFunc
+  def funcname = smtFunc.name
+  override def typ = smtFunc.typ
 }
 
 // --- Field and predicate accesses
diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index bb9345987..09bc8d805 100644
--- a/src/main/scala/viper/silver/ast/Program.scala
+++ b/src/main/scala/viper/silver/ast/Program.scala
@@ -734,7 +734,8 @@ case object NotOp extends UnOp with BoolDomainFunc {
 }
 
 
-case class SMTFunc(name: String, smtName: String, override val typ: Type, override val formalArgs: Seq[LocalVarDecl]) extends Node with AbstractDomainFunc with BuiltinDomainFunc
+case class SMTFunc(name: String, smtName: String, override val typ: Type, override val formalArgs: Seq[LocalVarDecl])
+  extends Node with AbstractDomainFunc with BuiltinDomainFunc
 
 /**
   * The Extension Member trait provides the way to expand the Ast to include new Top Level declarations
diff --git a/src/main/scala/viper/silver/testing/SMTTypeTest.scala b/src/main/scala/viper/silver/testing/SMTTypeTest.scala
new file mode 100644
index 000000000..824052586
--- /dev/null
+++ b/src/main/scala/viper/silver/testing/SMTTypeTest.scala
@@ -0,0 +1,165 @@
+package viper.silver.testing
+
+import org.scalatest.{BeforeAndAfterAllConfigMap, ConfigMap, FunSuite, Matchers}
+import viper.silver.ast.{AnySetContains, Assert, EqCmp, Field, FieldAccess, FieldAccessPredicate, FullPerm, Inhale, IntLit, LocalVarAssign, LocalVarDecl, Method, Program, Ref, SMTFuncApp, Seqn, SetType, Stmt}
+import viper.silver.ast.utility.{BVFactory, FloatFactory, RoundingMode}
+import viper.silver.verifier.{Failure, Success, Verifier}
+import viper.silver.verifier.errors.AssertFailed
+
+trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap {
+
+  def generateTypeCombinationTest(success: Boolean) : (Program, Assert) = {
+    val t = if (success) BVFactory(23).typ else FloatFactory(23, 11, RoundingMode.RNE).typ
+    val p1_decl = LocalVarDecl("three", t)()
+    val p1_ref = p1_decl.localVar
+    val p2_decl = LocalVarDecl("lol", SetType(t))()
+    val p2_ref= p2_decl.localVar
+    val element_in_param = AnySetContains(p1_ref, p2_ref)()
+
+    val assume = Inhale(element_in_param)()
+    val assert = Assert(element_in_param)()
+    val body = if (success) Seq(assume, assert) else Seq(assert)
+    (wrapInProgram(body, Seq(p1_decl, p2_decl), Seq()), assert)
+  }
+
+  def generateFieldTypeTest(success: Boolean) : (Program, Assert) = {
+    val t = if (!success) BVFactory(23).typ else FloatFactory(23, 11, RoundingMode.RNE).typ
+    val field = Field("f", t)()
+    val p1_decl = LocalVarDecl("three", Ref)()
+    val p1_ref = p1_decl.localVar
+    val p2_decl = LocalVarDecl("lol", SetType(t))()
+    val p2_ref= p2_decl.localVar
+    val fieldAcc = FieldAccess(p1_ref, field)()
+    val perm = FieldAccessPredicate(fieldAcc, FullPerm()())()
+    val element_in_param = AnySetContains(fieldAcc, p2_ref)()
+
+    val getPerm = Inhale(perm)()
+    val assume = Inhale(element_in_param)()
+    val assert = Assert(element_in_param)()
+    val body = if (success) Seq(getPerm, assume, assert) else Seq(getPerm, assert)
+    (wrapInProgram(body, Seq(p1_decl, p2_decl), Seq(), fields = Seq(field)), assert)
+  }
+
+  def generateFloatOpTest(success: Boolean) : (Program, Assert) = {
+    val rne = RoundingMode.RNE
+    val fp = FloatFactory(24, 8, rne)
+    val first = 1081081856 // 3.75
+    val second = 1103888384 // 25.5
+    val result = 1105854464 // 29.25
+    val bv32 = BVFactory(32)
+    val from_int = bv32.from_int("toBV32")
+    val to_fp = fp.from_bv("tofp")
+    val fp_eq = fp.eq("fp_eq")
+    val fp_add = fp.add("fp_add")
+
+    val first_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(first)()))()))()
+    val second_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(second)()))()))()
+    val result_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(result)()))()))()
+
+    val zero_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(0)()))()))()
+
+    val addition = SMTFuncApp(fp_add, Seq(first_float, second_float))()
+    val result_addition = SMTFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
+
+    val equality = SMTFuncApp(fp_eq, Seq(addition, result_addition))()
+    val assert = Assert(equality)()
+    (wrapInProgram(Seq(assert), Seq(), Seq()), assert)
+  }
+
+  def generateBvOpTest(success: Boolean) : (Program, Assert) = {
+    val bv23 = BVFactory(23)
+    val from_int = bv23.from_int("toBV23")
+    val two_lit = IntLit(2)()
+    val three_lit = IntLit(3)()
+    val one_lit = IntLit(1) ()
+    val two = SMTFuncApp(from_int, Seq(two_lit))()
+    val three = SMTFuncApp(from_int, Seq(three_lit))()
+    val one = SMTFuncApp(from_int, Seq(one_lit))()
+    val result_decl = LocalVarDecl("three", bv23.typ)()
+    val result_ref = result_decl.localVar
+    val assign = LocalVarAssign(result_ref, if (success) three else one)()
+    val xor = bv23.xor("xorBV23")
+    val xor_app = SMTFuncApp(xor, Seq(one, two))()
+    val equality1 = EqCmp(result_ref, xor_app)()
+    val assertion1 = Assert(equality1)()
+    (wrapInProgram(Seq(assign, assertion1), Seq(), Seq(result_decl)), assertion1)
+  }
+
+  def wrapInProgram(stmts: Seq[Stmt], params: Seq[LocalVarDecl], vars: Seq[LocalVarDecl], fields: Seq[Field] = Seq()): Program = {
+    val block = Seqn(stmts, vars)()
+    val method = Method("test", params, Seq(), Seq(), Seq(), Some(block))()
+    Program(Seq(), fields, Seq(), Seq(), Seq(method), Seq())()
+  }
+
+  val verifier : Verifier
+
+  override def beforeAll(configMap: ConfigMap) {
+    verifier.parseCommandLine(Seq("dummy.vpr"))
+    verifier.start()
+  }
+
+  override def afterAll(configMap: ConfigMap) {
+    verifier.stop()
+  }
+
+  test("typeCombinationSuccess") {
+    val (prog, assertNode) = generateTypeCombinationTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("typeCombinationFail") {
+    val (prog, assertNode) = generateTypeCombinationTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(AssertFailed(assertNode, _, _))) => true
+      case _ => false
+    })
+  }
+
+  test("fieldTypeSuccess") {
+    val (prog, assertNode) = generateFieldTypeTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("fieldTypeFail") {
+    val (prog, assertNode) = generateFieldTypeTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(AssertFailed(assertNode, _, _))) => true
+      case _ => false
+    })
+  }
+
+  test("bvOpSuccess") {
+    val (prog, assertNode) = generateBvOpTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("bvOpFail") {
+    val (prog, assertNode) = generateBvOpTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(AssertFailed(assertNode, _, _))) => true
+      case _ => false
+    })
+  }
+
+  test("floatOpSuccess") {
+    val (prog, assertNode) = generateFloatOpTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("floatOpFail") {
+    val (prog, assertNode) = generateFloatOpTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(AssertFailed(assertNode, _, _))) => true
+      case _ => false
+    })
+  }
+
+}

From 0b2718c2f248404816ccfe93c22c34da5ff600c7 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 24 Jul 2020 18:54:31 +0200
Subject: [PATCH 4/5] Added test for functions

---
 .../viper/silver/testing/SMTTypeTest.scala    | 55 +++++++++++++++++--
 1 file changed, 49 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/viper/silver/testing/SMTTypeTest.scala b/src/main/scala/viper/silver/testing/SMTTypeTest.scala
index 824052586..c0661540c 100644
--- a/src/main/scala/viper/silver/testing/SMTTypeTest.scala
+++ b/src/main/scala/viper/silver/testing/SMTTypeTest.scala
@@ -1,10 +1,10 @@
 package viper.silver.testing
 
 import org.scalatest.{BeforeAndAfterAllConfigMap, ConfigMap, FunSuite, Matchers}
-import viper.silver.ast.{AnySetContains, Assert, EqCmp, Field, FieldAccess, FieldAccessPredicate, FullPerm, Inhale, IntLit, LocalVarAssign, LocalVarDecl, Method, Program, Ref, SMTFuncApp, Seqn, SetType, Stmt}
+import viper.silver.ast.{AnySetContains, Assert, EqCmp, Exp, Field, FieldAccess, FieldAccessPredicate, FullPerm, Function, Inhale, IntLit, LocalVarAssign, LocalVarDecl, Method, Program, Ref, Result, SMTFuncApp, Seqn, SetType, Stmt}
 import viper.silver.ast.utility.{BVFactory, FloatFactory, RoundingMode}
 import viper.silver.verifier.{Failure, Success, Verifier}
-import viper.silver.verifier.errors.AssertFailed
+import viper.silver.verifier.errors.{AssertFailed, PostconditionViolated}
 
 trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap {
 
@@ -66,6 +66,34 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
     (wrapInProgram(Seq(assert), Seq(), Seq()), assert)
   }
 
+  def generateFloatOpFunctionTest(success: Boolean) : (Program, Function, Exp) = {
+    val rne = RoundingMode.RNE
+    val fp = FloatFactory(24, 8, rne)
+    val first = 1081081856 // 3.75
+    val second = 1103888384 // 25.5
+    val result = 1105854464 // 29.25
+    val bv32 = BVFactory(32)
+    val from_int = bv32.from_int("toBV32")
+    val to_fp = fp.from_bv("tofp")
+    val fp_eq = fp.eq("fp_eq")
+    val fp_add = fp.add("fp_add")
+
+    val first_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(first)()))()))()
+    val second_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(second)()))()))()
+    val result_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(result)()))()))()
+
+    val zero_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(0)()))()))()
+
+    val addition = SMTFuncApp(fp_add, Seq(first_float, second_float))()
+    val result_addition = SMTFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
+
+    val equality = SMTFuncApp(fp_eq, Seq(Result(fp.typ)(), result_addition))()
+
+    val fun = Function("test", Seq(), fp.typ, Seq(), Seq(equality), Some(addition))()
+    val program = Program(Seq(), Seq(), Seq(fun), Seq(), Seq(), Seq())()
+    (program, fun, equality)
+  }
+
   def generateBvOpTest(success: Boolean) : (Program, Assert) = {
     val bv23 = BVFactory(23)
     val from_int = bv23.from_int("toBV23")
@@ -112,7 +140,7 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
     val (prog, assertNode) = generateTypeCombinationTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(assertNode, _, _))) => true
+      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
       case _ => false
     })
   }
@@ -127,7 +155,7 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
     val (prog, assertNode) = generateFieldTypeTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(assertNode, _, _))) => true
+      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
       case _ => false
     })
   }
@@ -142,7 +170,7 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
     val (prog, assertNode) = generateBvOpTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(assertNode, _, _))) => true
+      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
       case _ => false
     })
   }
@@ -157,7 +185,22 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
     val (prog, assertNode) = generateFloatOpTest(false)
     val res  = verifier.verify(prog)
     assert(res match {
-      case Failure(Seq(AssertFailed(assertNode, _, _))) => true
+      case Failure(Seq(AssertFailed(a, _, _))) if a == assertNode => true
+      case _ => false
+    })
+  }
+
+  test("floatOpFunctionSuccess") {
+    val (prog, fun, exp) = generateFloatOpFunctionTest(true)
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
+  test("floatOpFunctionFail") {
+    val (prog, fun, exp) = generateFloatOpFunctionTest(false)
+    val res  = verifier.verify(prog)
+    assert(res match {
+      case Failure(Seq(PostconditionViolated(e, f, _, _))) if e == exp && fun == f => true
       case _ => false
     })
   }

From 075fd4ba75532b8160429815281fe263b535bac4 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sun, 10 Jan 2021 02:20:22 +0100
Subject: [PATCH 5/5] Renaming

---
 .../scala/viper/silver/ast/Expression.scala   | 12 +--
 src/main/scala/viper/silver/ast/Program.scala |  2 +-
 src/main/scala/viper/silver/ast/Type.scala    |  2 +-
 .../silver/ast/pretty/PrettyPrinter.scala     |  5 +-
 .../ast/utility/BackendTypeFactories.scala    | 73 +++++++++++++++++++
 .../silver/ast/utility/Expressions.scala      |  2 +-
 .../viper/silver/ast/utility/Nodes.scala      |  2 +-
 .../silver/ast/utility/SMTTypeFactories.scala | 73 -------------------
 .../viper/silver/ast/utility/Types.scala      |  2 +-
 ...MTTypeTest.scala => BackendTypeTest.scala} | 40 +++++-----
 10 files changed, 107 insertions(+), 106 deletions(-)
 create mode 100644 src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala
 delete mode 100644 src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala
 rename src/main/scala/viper/silver/testing/{SMTTypeTest.scala => BackendTypeTest.scala} (78%)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 067187926..21b5a5085 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -385,15 +385,15 @@ object DomainFuncApp {
     DomainFuncApp(func.name,args,typVarMap)(pos, info, func.typ.substitute(typVarMap), func.domainName, errT)
 }
 
-// --- References to built-in SMT Lib functions
+// --- References to backend (i.e., SMTLIB or Boogie 'builtin') functions
 
-case class SMTFuncApp(smtFunc: SMTFunc, args: Seq[Exp])
-                     (val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos)
+case class BackendFuncApp(backendFunc: BackendFunc, args: Seq[Exp])
+                         (val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos)
   extends AbstractDomainFuncApp {
   override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
-  override def func = (p: Program) => smtFunc
-  def funcname = smtFunc.name
-  override def typ = smtFunc.typ
+  override def func = (p: Program) => backendFunc
+  def funcname = backendFunc.name
+  override def typ = backendFunc.typ
 }
 
 // --- Field and predicate accesses
diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index 31392a9cd..387bfb336 100644
--- a/src/main/scala/viper/silver/ast/Program.scala
+++ b/src/main/scala/viper/silver/ast/Program.scala
@@ -771,7 +771,7 @@ case object NotOp extends UnOp with BoolDomainFunc {
 }
 
 
-case class SMTFunc(name: String, smtName: String, override val typ: Type, override val formalArgs: Seq[LocalVarDecl])
+case class BackendFunc(name: String, smtName: String, override val typ: Type, override val formalArgs: Seq[LocalVarDecl])
   extends Node with AbstractDomainFunc with BuiltinDomainFunc
 
 /**
diff --git a/src/main/scala/viper/silver/ast/Type.scala b/src/main/scala/viper/silver/ast/Type.scala
index a450c6295..101fef906 100644
--- a/src/main/scala/viper/silver/ast/Type.scala
+++ b/src/main/scala/viper/silver/ast/Type.scala
@@ -183,7 +183,7 @@ case class TypeVar(name: String) extends Type {
   //def !=(other: TypeVar) = name != other
 }
 
-case class SMTType(boogieName: String, smtName: String) extends AtomicType
+case class BackendType(boogieName: String, smtName: String) extends AtomicType
 
 trait ExtensionType extends Type{
   def getAstType: Type = ???
diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
index 57df288a1..dd4c4f941 100644
--- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -624,7 +624,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       case dt@DomainType(domainName, typVarsMap) =>
         val typArgs = dt.typeParameters map (t => show(typVarsMap.getOrElse(t, t)))
         text(domainName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char (',') <> space)))
-      case SMTType(boogieName, _) => boogieName
+      case BackendType(boogieName, _) if boogieName != null => boogieName
+      case BackendType(_, smtName) => smtName
     }
   }
 
@@ -775,7 +776,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
         parens(text(funcname) <> parens(ssep(args map show, char (',') <> space)) <> char(':') <+> show(dfa.typ))
       else
         text(funcname) <> parens(ssep(args map show, char (',') <> space))
-    case SMTFuncApp(func, args) =>
+    case BackendFuncApp(func, args) =>
       text(func.name) <> parens(ssep(args map show, char(',') <> space))
     case EmptySeq(elemTyp) =>
       text("Seq[") <> showType(elemTyp) <> "]()"
diff --git a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala
new file mode 100644
index 000000000..772b885b0
--- /dev/null
+++ b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala
@@ -0,0 +1,73 @@
+package viper.silver.ast.utility
+
+import viper.silver.ast.{Bool, Int, LocalVarDecl, BackendFunc, BackendType}
+
+/**
+  * A factory for fixed-size bitvectors that offers convenient access to bitvector types, as well as
+  * function definitions for unary and binary functions on bitvectors, as well as conversions from and
+  * to integers.
+  */
+case class BVFactory(size: Int) {
+  lazy val typ = BackendType(s"bv${size}", s"(_ BitVec ${size})")
+
+  def xor(name: String) = BackendFunc(name, "bvxor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def and(name: String) = BackendFunc(name, "bvand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def or(name: String) = BackendFunc(name, "bvor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def add(name: String) = BackendFunc(name, "bvadd", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def mul(name: String) = BackendFunc(name, "bvmul", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def shl(name: String) = BackendFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def shr(name: String) = BackendFunc(name, "bvshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def not(name: String) = BackendFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)()))
+  def neg(name: String) = BackendFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)()))
+
+  def from_int(name: String) = BackendFunc(name, s"(_ int2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
+  def to_int(name: String) = BackendFunc(name, s"(_ bv2int ${size})", Int, Seq(LocalVarDecl("x", typ)()))
+  def from_nat(name: String) = BackendFunc(name, s"(_ nat2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
+  def to_nat(name: String) = BackendFunc(name, s"(_ bv2nat ${size})", Int, Seq(LocalVarDecl("x", typ)()))
+}
+
+/**
+  * Rounding modes for floating point operations.
+  */
+object RoundingMode extends Enumeration {
+  type RoundingMode = Value
+  val RNE, RNA, RTP, RTN, RTZ = Value
+}
+import RoundingMode._
+
+/**
+  * A factory for IEEE floating point numbers with "exp" bits for the exponent, "mant" bits for the significant,
+  * including the hidden bit, and a given rounding mode for all operations that use one.
+  * Offers access to types, unary and binary operations, comparisons, and conversions from and to
+  * bitvectors of size exp + mant.
+  */
+case class FloatFactory(mant: Int, exp: Int, roundingMode: RoundingMode) {
+
+  lazy val typ = BackendType(s"float${mant}e${exp}", s"(_ FloatingPoint ${exp} ${mant})")
+
+  def neg(name: String) = BackendFunc(name, "fp.neg", typ, Seq(LocalVarDecl("x", typ)()))
+  def abs(name: String) = BackendFunc(name, "fp.abs", typ, Seq(LocalVarDecl("x", typ)()))
+
+  def add(name: String) = BackendFunc(name, s"fp.add ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def sub(name: String) = BackendFunc(name, s"fp.sub ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def mul(name: String) = BackendFunc(name, s"fp.mul ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def div(name: String) = BackendFunc(name, s"fp.div ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def min(name: String) = BackendFunc(name, s"fp.min ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def max(name: String) = BackendFunc(name, s"fp.max ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def eq(name: String) = BackendFunc(name, s"fp.eq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def leq(name: String) = BackendFunc(name, s"fp.leq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def geq(name: String) = BackendFunc(name, s"fp.geq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def lt(name: String) = BackendFunc(name, s"fp.lt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  def gt(name: String) = BackendFunc(name, s"fp.gt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+
+  def isZero(name: String) = BackendFunc(name, s"fp.isZero", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isInfinite(name: String) = BackendFunc(name, s"fp.isInfinite", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isNaN(name: String) = BackendFunc(name, s"fp.isNaN", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isNegative(name: String) = BackendFunc(name, s"fp.isNegative", Bool, Seq(LocalVarDecl("x", typ)()))
+  def isPositive(name: String) = BackendFunc(name, s"fp.isPositive", Bool, Seq(LocalVarDecl("x", typ)()))
+
+  def from_bv(name: String) = BackendFunc(name, s"(_ to_fp ${exp} ${mant}) ", typ, Seq(LocalVarDecl("x", BVFactory(mant+exp).typ)()))
+  def to_bv(name: String) = BackendFunc(name, s"(_ fp.to_sbv ${exp+mant}) ${roundingMode} ", BVFactory(mant+exp).typ, Seq(LocalVarDecl("x", typ)()))
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/ast/utility/Expressions.scala b/src/main/scala/viper/silver/ast/utility/Expressions.scala
index 723327322..6170bcf8e 100644
--- a/src/main/scala/viper/silver/ast/utility/Expressions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Expressions.scala
@@ -33,7 +33,7 @@ object Expressions {
          | _: PermExp
          | _: FuncApp
          | _: DomainFuncApp
-         | _: SMTFuncApp
+         | _: BackendFuncApp
          | _: LocationAccess
          | _: AbstractLocalVar
          | _: SeqExp
diff --git a/src/main/scala/viper/silver/ast/utility/Nodes.scala b/src/main/scala/viper/silver/ast/utility/Nodes.scala
index 95bc31606..10999e840 100644
--- a/src/main/scala/viper/silver/ast/utility/Nodes.scala
+++ b/src/main/scala/viper/silver/ast/utility/Nodes.scala
@@ -106,7 +106,7 @@ object Nodes {
           case FuncApp(_, args) => args
           case DomainFuncApp(_, args, m) =>
             args ++ m.keys ++ m.values
-          case SMTFuncApp(_, args) => args
+          case BackendFuncApp(_, args) => args
 
           case EmptySeq(elemTyp) => Seq(elemTyp)
           case ExplicitSeq(elems) => elems
diff --git a/src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala b/src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala
deleted file mode 100644
index 368784240..000000000
--- a/src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala
+++ /dev/null
@@ -1,73 +0,0 @@
-package viper.silver.ast.utility
-
-import viper.silver.ast.{Bool, Int, LocalVarDecl, SMTFunc, SMTType}
-
-/**
-  * A factory for fixed-size bitvectors that offers convenient access to bitvector types, as well as
-  * function definitions for unary and binary functions on bitvectors, as well as conversions from and
-  * to integers.
-  */
-case class BVFactory(size: Int) {
-  lazy val typ = SMTType(s"bv${size}", s"(_ BitVec ${size})")
-
-  def xor(name: String) = SMTFunc(name, "bvxor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def and(name: String) = SMTFunc(name, "bvand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def or(name: String) = SMTFunc(name, "bvor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def add(name: String) = SMTFunc(name, "bvadd", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def mul(name: String) = SMTFunc(name, "bvmul", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def shl(name: String) = SMTFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def shr(name: String) = SMTFunc(name, "bvshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-
-  def not(name: String) = SMTFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)()))
-  def neg(name: String) = SMTFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)()))
-
-  def from_int(name: String) = SMTFunc(name, s"(_ int2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
-  def to_int(name: String) = SMTFunc(name, s"(_ bv2int ${size})", Int, Seq(LocalVarDecl("x", typ)()))
-  def from_nat(name: String) = SMTFunc(name, s"(_ nat2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
-  def to_nat(name: String) = SMTFunc(name, s"(_ bv2nat ${size})", Int, Seq(LocalVarDecl("x", typ)()))
-}
-
-/**
-  * Rounding modes for floating point operations.
-  */
-object RoundingMode extends Enumeration {
-  type RoundingMode = Value
-  val RNE, RNA, RTP, RTN, RTZ = Value
-}
-import RoundingMode._
-
-/**
-  * A factory for IEEE floating point numbers with "exp" bits for the exponent, "mant" bits for the significant,
-  * including the hidden bit, and a given rounding mode for all operations that use one.
-  * Offers access to types, unary and binary operations, comparisons, and conversions from and to
-  * bitvectors of size exp + mant.
-  */
-case class FloatFactory(mant: Int, exp: Int, roundingMode: RoundingMode) {
-
-  lazy val typ = SMTType(s"float${mant}e${exp}", s"(_ FloatingPoint ${exp} ${mant})")
-
-  def neg(name: String) = SMTFunc(name, "fp.neg", typ, Seq(LocalVarDecl("x", typ)()))
-  def abs(name: String) = SMTFunc(name, "fp.abs", typ, Seq(LocalVarDecl("x", typ)()))
-
-  def add(name: String) = SMTFunc(name, s"fp.add ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def sub(name: String) = SMTFunc(name, s"fp.sub ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def mul(name: String) = SMTFunc(name, s"fp.mul ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def div(name: String) = SMTFunc(name, s"fp.div ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def min(name: String) = SMTFunc(name, s"fp.min ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def max(name: String) = SMTFunc(name, s"fp.max ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-
-  def eq(name: String) = SMTFunc(name, s"fp.eq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def leq(name: String) = SMTFunc(name, s"fp.leq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def geq(name: String) = SMTFunc(name, s"fp.geq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def lt(name: String) = SMTFunc(name, s"fp.lt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def gt(name: String) = SMTFunc(name, s"fp.gt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-
-  def isZero(name: String) = SMTFunc(name, s"fp.isZero", Bool, Seq(LocalVarDecl("x", typ)()))
-  def isInfinite(name: String) = SMTFunc(name, s"fp.isInfinite", Bool, Seq(LocalVarDecl("x", typ)()))
-  def isNaN(name: String) = SMTFunc(name, s"fp.isNaN", Bool, Seq(LocalVarDecl("x", typ)()))
-  def isNegative(name: String) = SMTFunc(name, s"fp.isNegative", Bool, Seq(LocalVarDecl("x", typ)()))
-  def isPositive(name: String) = SMTFunc(name, s"fp.isPositive", Bool, Seq(LocalVarDecl("x", typ)()))
-
-  def from_bv(name: String) = SMTFunc(name, s"(_ to_fp ${exp} ${mant}) ", typ, Seq(LocalVarDecl("x", BVFactory(mant+exp).typ)()))
-  def to_bv(name: String) = SMTFunc(name, s"(_ fp.to_sbv ${exp+mant}) ${roundingMode} ", BVFactory(mant+exp).typ, Seq(LocalVarDecl("x", typ)()))
-}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/ast/utility/Types.scala b/src/main/scala/viper/silver/ast/utility/Types.scala
index 11a57305f..d2e3fb440 100644
--- a/src/main/scala/viper/silver/ast/utility/Types.scala
+++ b/src/main/scala/viper/silver/ast/utility/Types.scala
@@ -69,7 +69,7 @@ object Types {
     * @return The list of transitive type constituents of `typ`.
     */
   def typeConstituents(typ: Type): List[Type] = typ match {
-    case Int | Bool | Perm | Ref | InternalType | _: TypeVar | Wand | _: SMTType => Nil
+    case Int | Bool | Perm | Ref | InternalType | _: TypeVar | Wand | _: BackendType => Nil
     case dt: DomainType => dt.typeParameters.map(_.substitute(dt.typVarsMap)).toList
     case SeqType(elementType) => elementType :: typeConstituents(elementType)
     case SetType(elementType) => elementType :: typeConstituents(elementType)
diff --git a/src/main/scala/viper/silver/testing/SMTTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
similarity index 78%
rename from src/main/scala/viper/silver/testing/SMTTypeTest.scala
rename to src/main/scala/viper/silver/testing/BackendTypeTest.scala
index c0661540c..b213744fe 100644
--- a/src/main/scala/viper/silver/testing/SMTTypeTest.scala
+++ b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
@@ -1,12 +1,12 @@
 package viper.silver.testing
 
 import org.scalatest.{BeforeAndAfterAllConfigMap, ConfigMap, FunSuite, Matchers}
-import viper.silver.ast.{AnySetContains, Assert, EqCmp, Exp, Field, FieldAccess, FieldAccessPredicate, FullPerm, Function, Inhale, IntLit, LocalVarAssign, LocalVarDecl, Method, Program, Ref, Result, SMTFuncApp, Seqn, SetType, Stmt}
+import viper.silver.ast.{AnySetContains, Assert, EqCmp, Exp, Field, FieldAccess, FieldAccessPredicate, FullPerm, Function, Inhale, IntLit, LocalVarAssign, LocalVarDecl, Method, Program, Ref, Result, BackendFuncApp, Seqn, SetType, Stmt}
 import viper.silver.ast.utility.{BVFactory, FloatFactory, RoundingMode}
 import viper.silver.verifier.{Failure, Success, Verifier}
 import viper.silver.verifier.errors.{AssertFailed, PostconditionViolated}
 
-trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap {
+trait BackendTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap {
 
   def generateTypeCombinationTest(success: Boolean) : (Program, Assert) = {
     val t = if (success) BVFactory(23).typ else FloatFactory(23, 11, RoundingMode.RNE).typ
@@ -52,16 +52,16 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
     val fp_eq = fp.eq("fp_eq")
     val fp_add = fp.add("fp_add")
 
-    val first_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(first)()))()))()
-    val second_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(second)()))()))()
-    val result_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(result)()))()))()
+    val first_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(first)()))()))()
+    val second_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(second)()))()))()
+    val result_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(result)()))()))()
 
-    val zero_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(0)()))()))()
+    val zero_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(0)()))()))()
 
-    val addition = SMTFuncApp(fp_add, Seq(first_float, second_float))()
-    val result_addition = SMTFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
+    val addition = BackendFuncApp(fp_add, Seq(first_float, second_float))()
+    val result_addition = BackendFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
 
-    val equality = SMTFuncApp(fp_eq, Seq(addition, result_addition))()
+    val equality = BackendFuncApp(fp_eq, Seq(addition, result_addition))()
     val assert = Assert(equality)()
     (wrapInProgram(Seq(assert), Seq(), Seq()), assert)
   }
@@ -78,16 +78,16 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
     val fp_eq = fp.eq("fp_eq")
     val fp_add = fp.add("fp_add")
 
-    val first_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(first)()))()))()
-    val second_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(second)()))()))()
-    val result_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(result)()))()))()
+    val first_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(first)()))()))()
+    val second_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(second)()))()))()
+    val result_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(result)()))()))()
 
-    val zero_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(0)()))()))()
+    val zero_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(0)()))()))()
 
-    val addition = SMTFuncApp(fp_add, Seq(first_float, second_float))()
-    val result_addition = SMTFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
+    val addition = BackendFuncApp(fp_add, Seq(first_float, second_float))()
+    val result_addition = BackendFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
 
-    val equality = SMTFuncApp(fp_eq, Seq(Result(fp.typ)(), result_addition))()
+    val equality = BackendFuncApp(fp_eq, Seq(Result(fp.typ)(), result_addition))()
 
     val fun = Function("test", Seq(), fp.typ, Seq(), Seq(equality), Some(addition))()
     val program = Program(Seq(), Seq(), Seq(fun), Seq(), Seq(), Seq())()
@@ -100,14 +100,14 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
     val two_lit = IntLit(2)()
     val three_lit = IntLit(3)()
     val one_lit = IntLit(1) ()
-    val two = SMTFuncApp(from_int, Seq(two_lit))()
-    val three = SMTFuncApp(from_int, Seq(three_lit))()
-    val one = SMTFuncApp(from_int, Seq(one_lit))()
+    val two = BackendFuncApp(from_int, Seq(two_lit))()
+    val three = BackendFuncApp(from_int, Seq(three_lit))()
+    val one = BackendFuncApp(from_int, Seq(one_lit))()
     val result_decl = LocalVarDecl("three", bv23.typ)()
     val result_ref = result_decl.localVar
     val assign = LocalVarAssign(result_ref, if (success) three else one)()
     val xor = bv23.xor("xorBV23")
-    val xor_app = SMTFuncApp(xor, Seq(one, two))()
+    val xor_app = BackendFuncApp(xor, Seq(one, two))()
     val equality1 = EqCmp(result_ref, xor_app)()
     val assertion1 = Assert(equality1)()
     (wrapInProgram(Seq(assign, assertion1), Seq(), Seq(result_decl)), assertion1)