GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/api/reset_assertions.cpp Lines: 20 20 100.0 %
Date: 2021-03-22 Branches: 28 56 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file reset_assertions.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Mudathir Mohamed
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief A simple test for SmtEngine::resetAssertions()
13
 **
14
 ** This program indirectly also tests some corner cases w.r.t.
15
 ** context-dependent datastructures: resetAssertions() pops the contexts to
16
 ** zero but some context-dependent datastructures are created at leevel 1,
17
 ** which the datastructure needs to handle properly problematic.
18
 **/
19
20
#include <iostream>
21
#include <sstream>
22
23
#include "api/cvc4cpp.h"
24
25
using namespace CVC4::api;
26
27
1
int main()
28
{
29
2
  Solver slv;
30
1
  slv.setOption("incremental", "true");
31
32
2
  Sort real = slv.getRealSort();
33
2
  Term x = slv.mkConst(real, "x");
34
2
  Term four = slv.mkInteger(4);
35
2
  Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
36
1
  slv.assertFormula(xEqFour);
37
1
  std::cout << slv.checkSat() << std::endl;
38
39
1
  slv.resetAssertions();
40
41
2
  Sort elementType = slv.getIntegerSort();
42
2
  Sort indexType = slv.getIntegerSort();
43
2
  Sort arrayType = slv.mkArraySort(indexType, elementType);
44
2
  Term array = slv.mkConst(arrayType, "array");
45
2
  Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
46
2
  Term ten = slv.mkInteger(10);
47
2
  Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
48
1
  slv.assertFormula(arrayAtFour_eq_ten);
49
1
  std::cout << slv.checkSat() << std::endl;
50
4
}