| /*******************************************************************************
|
| * Copyright (c) 2016 CEA LIST.
|
| *
|
| * All rights reserved. This program and the accompanying materials
|
| * are made available under the terms of the Eclipse Public License v1.0
|
| * which accompanies this distribution, and is available at
|
| * http://www.eclipse.org/legal/epl-v10.html
|
| *
|
| * Created on: 06 july 2016
|
| *
|
| * Contributors:
|
| * Stephane Salmons (CEA LIST) stephane.salmons@gmail.com
|
| * - Initial API and Implementation
|
| ******************************************************************************/
|
| /*
|
| * Yices 2 is an SMT solver that decides the satisfiability of
|
| * formulas containing uninterpreted function symbols with equality,
|
| * linear real and integer arithmetic, bitvectors, scalar types, and tuples.
|
| * http://yices.csl.sri.com/
|
| *
|
| */
|
|
|
|
|
| /*
|
|
|
| test on optional library that is not yet integrated into diversity install process
|
|
|
|
|
| * /
|
|
|
|
|
|
|
| /*
|
| #include "boost/test/unit_test.hpp"
|
|
|
| #include <common/BF.h> |
| |
| #include <fml/expression/ExpressionConstructor.h> |
| #include <fml/executable/InstanceOfData.h> |
| |
| #include <fml/type/TypeManager.h> |
| |
| #include <compat/model/xbed/XBED.h>
|
|
|
| #include <yices2/yices.h>
|
|
|
|
|
| using namespace std;
|
| using namespace sep;
|
|
|
| BOOST_AUTO_TEST_SUITE(FML);
|
|
|
| BOOST_AUTO_TEST_CASE(t_yices_expression_printing) {
|
|
|
| BOOST_CHECK_MESSAGE(true, "yices dummy test");
|
| }
|
|
|
| BOOST_AUTO_TEST_SUITE_END(); // FML
|
|
|
|
|
| */
|
