google test: util: Migrate integer_white. (#6024)
[cvc5.git] / test / unit / util / array_store_all_white.h
index fb7857003457755358b6f3b365f81f5f9ac7186f..2e107f6687b472cdcac8b6dd4b5ea7b5fc1e86b5 100644 (file)
@@ -2,10 +2,10 @@
 /*! \file array_store_all_white.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Mathias Preiner
+ **   Andres Noetzli, Morgan Deters, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -50,7 +50,7 @@ class ArrayStoreAllWhite : public CxxTest::TestSuite
     ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->realType()),
                   d_nm->mkConst(Rational(9, 2)));
     ArrayStoreAll(d_nm->mkArrayType(d_nm->mkSort("U"), usort),
-                  d_nm->mkConst(UninterpretedConstant(usort.toType(), 0)));
+                  d_nm->mkConst(UninterpretedConstant(usort, 0)));
     ArrayStoreAll(d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->realType()),
                   d_nm->mkConst(Rational(0)));
     ArrayStoreAll(
@@ -62,7 +62,7 @@ class ArrayStoreAllWhite : public CxxTest::TestSuite
   {
     TS_ASSERT_THROWS(ArrayStoreAll(d_nm->integerType(),
                                    d_nm->mkConst(UninterpretedConstant(
-                                       d_nm->mkSort("U").toType(), 0))),
+                                       d_nm->mkSort("U"), 0))),
                      IllegalArgumentException&);
     TS_ASSERT_THROWS(
         ArrayStoreAll(d_nm->integerType(), d_nm->mkConst(Rational(9, 2))),