File: proj-issue611.cpp

package info (click to toggle)
cvc5 1.1.2-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 80,856 kB
  • sloc: cpp: 339,634; java: 10,248; python: 10,063; sh: 6,726; ansic: 1,622; lisp: 763; perl: 207; makefile: 33
file content (34 lines) | stat: -rw-r--r-- 961 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
/******************************************************************************
 * Top contributors (to current version):
 *   Yoni Zohar
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2023 by the authors listed in the file AUTHORS
 * 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.
 * ****************************************************************************
 *
 * Test for project issue #611
 *
 */
#include <cvc5/cvc5.h>

using namespace cvc5;
int main(void)
{
  Solver solver;
  solver.setOption("incremental", "false");
  solver.setOption("solve-bv-as-int", "bitwise");
  // should throw an exception due to the usage of an illegal value
  // (0) for the option
  try
  {
    solver.setOption("bvand-integer-granularity", "0");
  }
  catch (cvc5::CVC5ApiOptionException& e)
  {
  }
  return 0;
}