/*! \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
**
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(
{
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))),