Quickstart Guide
The primary input language for cvc5 is SMT-LIB v2 . We give a short explanation of the SMT-LIB v2 quickstart example here.
First, we set the logic.
The simplest way to set a logic for the solver is to choose “ALL”.
This enables all logics in the solver.
Alternatively,
"QF_ALL"
enables all logics without quantifiers.
To optimize the solver’s behavior for a more specific logic,
use the logic name, e.g.
"QF_BV"
or
"QF_AUFBV"
.
(set-logic ALL)
We will ask the solver to produce models and unsat cores in the following,
and for this we have to enable the following options.
Furthermore, we enable incremental solving so that we can use the
(reset-assertions)
command later on.
(set-option :produce-models true)
(set-option :incremental true)
; print unsat cores, include assertions in the unsat core that have not been named
(set-option :produce-unsat-cores true)
(set-option :dump-unsat-cores-full true)
Now, we create two constants
x
and
y
of sort
Real
.
Notice that these are
symbolic
constants, but not actual values.
; Declare real constants x,y
(declare-const x Real)
(declare-const y Real)
We define the following constraints regarding
x
and
y
:
\[(0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)\]
We assert them as follows. Notice that in SMT-LIB v2, terms are written in prefix notation, e.g., we write (+ x y) instead of (x + y) .
; Our constraints regarding x and y will be:
;
; (1) 0 < x
; (2) 0 < y
; (3) x + y < 1
; (4) x <= y
(assert (< 0 x))
(assert (< 0 y))
(assert (< (+ x y) 1))
(assert (<= x y))
Now we check if the asserted formula is satisfiable, that is, we check if
there exist values of sort
Real
for
x
and
y
that satisfy all
the constraints.
(check-sat)
The result we get from this satisfiability check is either
sat
,
unsat
or
unknown
, and it is printed to standard output.
In this case, it will print
sat
.
Now, we query the solver for the values for
x
and
y
that satisfy
the constraints.
It is also possible to get values for terms that do not appear in the original
formula.
(echo "Values of declared real constants and of compound terms built with them.")
(get-value (x y (- x y)))
This will print the values of x , y , and x-y , in a key-value format (<term> <value>) one after the other:
((x (/ 1 6)) (y (/ 1 6)) ((- x y) 0.0))
Next, we will check satisfiability of the same formula,
only this time over integer variables
a
and
b
.
For this, we first reset the assertions added to the solver and declare fresh
integer variables
a
and
b
.
(echo "We will reset the solver with the (reset-assertions) command and check satisfiability of the same assertions but with the integers constants rather than with the real ones.")
(reset-assertions)
; Declare integer constants a,b
(declare-const a Int)
(declare-const b Int)
Next, we assert the same assertions as above, but with integers.
(assert (< 0 a))
(assert (< 0 b))
(assert (< (+ a b) 1))
(assert (<= a b))
Now, we check whether the revised query is satisfiable.
(check-sat)
This time the asserted formula is unsatisfiable and
unsat
is printed.
We can query the solver for an unsatisfiable core, that is, a subset of the assertions that is already unsatisfiable.
(get-unsat-core)
This will print:
(
(< 0 a)
(< 0 b)
(< (+ a b) 1)
)
Example
examples/api/smtlib/quickstart.smt2
1 (set-logic ALL)
2 (set-option :produce-models true)
3 (set-option :incremental true)
4 ; print unsat cores, include assertions in the unsat core that have not been named
5 (set-option :produce-unsat-cores true)
6 (set-option :dump-unsat-cores-full true)
7
8 ; Declare real constants x,y
9 (declare-const x Real)
10 (declare-const y Real)
11
12 ; Our constraints regarding x and y will be:
13 ;
14 ; (1) 0 < x
15 ; (2) 0 < y
16 ; (3) x + y < 1
17 ; (4) x <= y
18
19 (assert (< 0 x))
20 (assert (< 0 y))
21 (assert (< (+ x y) 1))
22 (assert (<= x y))
23
24 (check-sat)
25 (echo "Values of declared real constants and of compound terms built with them.")
26 (get-value (x y (- x y)))
27
28 (echo "We will reset the solver with the (reset-assertions) command and check satisfiability of the same assertions but with the integers constants rather than with the real ones.")
29 (reset-assertions)
30 ; Declare integer constants a,b
31 (declare-const a Int)
32 (declare-const b Int)
33 (assert (< 0 a))
34 (assert (< 0 b))
35 (assert (< (+ a b) 1))
36 (assert (<= a b))
37
38 (check-sat)
39 (get-unsat-core)
examples/api/cpp/quickstart.cpp
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Yoni Zohar, Gereon Kremer, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the api capabilities of cvc5.
14 *
15 */
16
17 #include <cvc5/cvc5.h>
18
19 #include <iostream>
20 #include <numeric>
21
22 using namespace cvc5;
23
24 int main()
25 {
26 // Create a solver
27 Solver solver;
28
29 // We will ask the solver to produce models and unsat cores,
30 // hence these options should be turned on.
31 solver.setOption("produce-models", "true");
32 solver.setOption("produce-unsat-cores", "true");
33
34 // The simplest way to set a logic for the solver is to choose "ALL".
35 // This enables all logics in the solver.
36 // Alternatively, "QF_ALL" enables all logics without quantifiers.
37 // To optimize the solver's behavior for a more specific logic,
38 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
39
40 // Set the logic
41 solver.setLogic("ALL");
42
43 // In this example, we will define constraints over reals and integers.
44 // Hence, we first obtain the corresponding sorts.
45 Sort realSort = solver.getRealSort();
46 Sort intSort = solver.getIntegerSort();
47
48 // x and y will be real variables, while a and b will be integer variables.
49 // Formally, their cpp type is Term,
50 // and they are called "constants" in SMT jargon:
51 Term x = solver.mkConst(realSort, "x");
52 Term y = solver.mkConst(realSort, "y");
53 Term a = solver.mkConst(intSort, "a");
54 Term b = solver.mkConst(intSort, "b");
55
56 // Our constraints regarding x and y will be:
57 //
58 // (1) 0 < x
59 // (2) 0 < y
60 // (3) x + y < 1
61 // (4) x <= y
62 //
63
64 // Formally, constraints are also terms. Their sort is Boolean.
65 // We will construct these constraints gradually,
66 // by defining each of their components.
67 // We start with the constant numerals 0 and 1:
68 Term zero = solver.mkReal(0);
69 Term one = solver.mkReal(1);
70
71 // Next, we construct the term x + y
72 Term xPlusY = solver.mkTerm(ADD, {x, y});
73
74 // Now we can define the constraints.
75 // They use the operators +, <=, and <.
76 // In the API, these are denoted by ADD, LEQ, and LT.
77 // A list of available operators is available in:
78 // src/api/cpp/cvc5_kind.h
79 Term constraint1 = solver.mkTerm(LT, {zero, x});
80 Term constraint2 = solver.mkTerm(LT, {zero, y});
81 Term constraint3 = solver.mkTerm(LT, {xPlusY, one});
82 Term constraint4 = solver.mkTerm(LEQ, {x, y});
83
84 // Now we assert the constraints to the solver.
85 solver.assertFormula(constraint1);
86 solver.assertFormula(constraint2);
87 solver.assertFormula(constraint3);
88 solver.assertFormula(constraint4);
89
90 // Check if the formula is satisfiable, that is,
91 // are there real values for x and y that satisfy all the constraints?
92 Result r1 = solver.checkSat();
93
94 // The result is either SAT, UNSAT, or UNKNOWN.
95 // In this case, it is SAT.
96 std::cout << "expected: sat" << std::endl;
97 std::cout << "result: " << r1 << std::endl;
98
99 // We can get the values for x and y that satisfy the constraints.
100 Term xVal = solver.getValue(x);
101 Term yVal = solver.getValue(y);
102
103 // It is also possible to get values for compound terms,
104 // even if those did not appear in the original formula.
105 Term xMinusY = solver.mkTerm(SUB, {x, y});
106 Term xMinusYVal = solver.getValue(xMinusY);
107
108 // We can now obtain the string representations of the values.
109 std::string xStr = xVal.getRealValue();
110 std::string yStr = yVal.getRealValue();
111 std::string xMinusYStr = xMinusYVal.getRealValue();
112
113 std::cout << "value for x: " << xStr << std::endl;
114 std::cout << "value for y: " << yStr << std::endl;
115 std::cout << "value for x - y: " << xMinusYStr << std::endl;
116
117 // Further, we can convert the values to cpp types
118 std::pair<int64_t, uint64_t> xPair = xVal.getReal64Value();
119 std::pair<int64_t, uint64_t> yPair = yVal.getReal64Value();
120 std::pair<int64_t, uint64_t> xMinusYPair = xMinusYVal.getReal64Value();
121
122 std::cout << "value for x: " << xPair.first << "/" << xPair.second << std::endl;
123 std::cout << "value for y: " << yPair.first << "/" << yPair.second << std::endl;
124 std::cout << "value for x - y: " << xMinusYPair.first << "/" << xMinusYPair.second << std::endl;
125
126 // Another way to independently compute the value of x - y would be
127 // to perform the (rational) arithmetic manually.
128 // However, for more complex terms,
129 // it is easier to let the solver do the evaluation.
130 std::pair<int64_t, uint64_t> xMinusYComputed = {
131 xPair.first * yPair.second - xPair.second * yPair.first,
132 xPair.second * yPair.second
133 };
134 uint64_t g = std::gcd(xMinusYComputed.first, xMinusYComputed.second);
135 xMinusYComputed = { xMinusYComputed.first / g, xMinusYComputed.second / g };
136 if (xMinusYComputed == xMinusYPair)
137 {
138 std::cout << "computed correctly" << std::endl;
139 }
140 else
141 {
142 std::cout << "computed incorrectly" << std::endl;
143 }
144
145 // Next, we will check satisfiability of the same formula,
146 // only this time over integer variables a and b.
147
148 // We start by resetting assertions added to the solver.
149 solver.resetAssertions();
150
151 // Next, we assert the same assertions above with integers.
152 // This time, we inline the construction of terms
153 // to the assertion command.
154 solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), a}));
155 solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), b}));
156 solver.assertFormula(
157 solver.mkTerm(LT, {solver.mkTerm(ADD, {a, b}), solver.mkInteger(1)}));
158 solver.assertFormula(solver.mkTerm(LEQ, {a, b}));
159
160 // We check whether the revised assertion is satisfiable.
161 Result r2 = solver.checkSat();
162
163 // This time the formula is unsatisfiable
164 std::cout << "expected: unsat" << std::endl;
165 std::cout << "result: " << r2 << std::endl;
166
167 // We can query the solver for an unsatisfiable core, i.e., a subset
168 // of the assertions that is already unsatisfiable.
169 std::vector<Term> unsatCore = solver.getUnsatCore();
170 std::cout << "unsat core size: " << unsatCore.size() << std::endl;
171 std::cout << "unsat core: " << std::endl;
172 for (const Term& t : unsatCore)
173 {
174 std::cout << t << std::endl;
175 }
176
177 return 0;
178 }
examples/api/java/QuickStart.java
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Aina Niemetz, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the api capabilities of cvc5.
14 *
15 */
16
17 import io.github.cvc5.*;
18 import java.math.BigInteger;
19 import java.util.ArrayList;
20 import java.util.Arrays;
21 import java.util.List;
22
23 public class QuickStart
24 {
25 public static void main(String args[]) throws CVC5ApiException
26 {
27 // Create a solver
28 try (Solver solver = new Solver())
29 {
30 // We will ask the solver to produce models and unsat cores,
31 // hence these options should be turned on.
32 solver.setOption("produce-models", "true");
33 solver.setOption("produce-unsat-cores", "true");
34
35 // The simplest way to set a logic for the solver is to choose "ALL".
36 // This enables all logics in the solver.
37 // Alternatively, "QF_ALL" enables all logics without quantifiers.
38 // To optimize the solver's behavior for a more specific logic,
39 // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
40
41 // Set the logic
42 solver.setLogic("ALL");
43
44 // In this example, we will define constraints over reals and integers.
45 // Hence, we first obtain the corresponding sorts.
46 Sort realSort = solver.getRealSort();
47 Sort intSort = solver.getIntegerSort();
48
49 // x and y will be real variables, while a and b will be integer variables.
50 // Formally, their cpp type is Term,
51 // and they are called "constants" in SMT jargon:
52 Term x = solver.mkConst(realSort, "x");
53 Term y = solver.mkConst(realSort, "y");
54 Term a = solver.mkConst(intSort, "a");
55 Term b = solver.mkConst(intSort, "b");
56
57 // Our constraints regarding x and y will be:
58 //
59 // (1) 0 < x
60 // (2) 0 < y
61 // (3) x + y < 1
62 // (4) x <= y
63 //
64
65 // Formally, constraints are also terms. Their sort is Boolean.
66 // We will construct these constraints gradually,
67 // by defining each of their components.
68 // We start with the constant numerals 0 and 1:
69 Term zero = solver.mkReal(0);
70 Term one = solver.mkReal(1);
71
72 // Next, we construct the term x + y
73 Term xPlusY = solver.mkTerm(Kind.ADD, x, y);
74
75 // Now we can define the constraints.
76 // They use the operators +, <=, and <.
77 // In the API, these are denoted by ADD, LEQ, and LT.
78 // A list of available operators is available in:
79 // src/api/cpp/cvc5_kind.h
80 Term constraint1 = solver.mkTerm(Kind.LT, zero, x);
81 Term constraint2 = solver.mkTerm(Kind.LT, zero, y);
82 Term constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
83 Term constraint4 = solver.mkTerm(Kind.LEQ, x, y);
84
85 // Now we assert the constraints to the solver.
86 solver.assertFormula(constraint1);
87 solver.assertFormula(constraint2);
88 solver.assertFormula(constraint3);
89 solver.assertFormula(constraint4);
90
91 // Check if the formula is satisfiable, that is,
92 // are there real values for x and y that satisfy all the constraints?
93 Result r1 = solver.checkSat();
94
95 // The result is either SAT, UNSAT, or UNKNOWN.
96 // In this case, it is SAT.
97 System.out.println("expected: sat");
98 System.out.println("result: " + r1);
99
100 // We can get the values for x and y that satisfy the constraints.
101 Term xVal = solver.getValue(x);
102 Term yVal = solver.getValue(y);
103
104 // It is also possible to get values for compound terms,
105 // even if those did not appear in the original formula.
106 Term xMinusY = solver.mkTerm(Kind.SUB, x, y);
107 Term xMinusYVal = solver.getValue(xMinusY);
108
109 // Further, we can convert the values to java types
110 Pair<BigInteger, BigInteger> xPair = xVal.getRealValue();
111 Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
112 Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();
113
114 System.out.println("value for x: " + xPair.first + "/" + xPair.second);
115 System.out.println("value for y: " + yPair.first + "/" + yPair.second);
116 System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second);
117
118 // Another way to independently compute the value of x - y would be
119 // to perform the (rational) arithmetic manually.
120 // However, for more complex terms,
121 // it is easier to let the solver do the evaluation.
122 Pair<BigInteger, BigInteger> xMinusYComputed =
123 new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
124 xPair.second.multiply(yPair.second));
125 BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second);
126 xMinusYComputed = new Pair(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g));
127 if (xMinusYComputed.equals(xMinusYPair))
128 {
129 System.out.println("computed correctly");
130 }
131 else
132 {
133 System.out.println("computed incorrectly");
134 }
135
136 // Next, we will check satisfiability of the same formula,
137 // only this time over integer variables a and b.
138
139 // We start by resetting assertions added to the solver.
140 solver.resetAssertions();
141
142 // Next, we assert the same assertions above with integers.
143 // This time, we inline the construction of terms
144 // to the assertion command.
145 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
146 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
147 solver.assertFormula(
148 solver.mkTerm(Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
149 solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
150
151 // We check whether the revised assertion is satisfiable.
152 Result r2 = solver.checkSat();
153
154 // This time the formula is unsatisfiable
155 System.out.println("expected: unsat");
156 System.out.println("result: " + r2);
157
158 // We can query the solver for an unsatisfiable core, i.e., a subset
159 // of the assertions that is already unsatisfiable.
160 List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
161 System.out.println("unsat core size: " + unsatCore.size());
162 System.out.println("unsat core: ");
163 for (Term t : unsatCore)
164 {
165 System.out.println(t);
166 }
167 }
168 }
169 }
cvc5_pythonic_api:/test/pgms/example_quickstart.py
1 from cvc5_pythonic_api import *
2
3 if __name__ == '__main__':
4
5 # Let's introduce some variables
6 x, y = Reals('x y')
7 a, b = Ints('a b')
8
9 # We will confirm that
10 # * 0 < x
11 # * 0 < y
12 # * x + y < 1
13 # * x <= y
14 # are satisfiable
15 solve(0 < x, 0 < y, x + y < 1, x <= y)
16
17 # If we get the model (the satisfying assignment) explicitly, we can
18 # evaluate terms under it.
19 s = Solver()
20 s.add(0 < x, 0 < y, x + y < 1, x <= y)
21 assert sat == s.check()
22 m = s.model()
23
24 print('x:', m[x])
25 print('y:', m[y])
26 print('x - y:', m[x - y])
27
28 # We can also get these values in other forms:
29 print('string x:', str(m[x]))
30 print('decimal x:', m[x].as_decimal(4))
31 print('fraction x:', m[x].as_fraction())
32 print('float x:', float(m[x].as_fraction()))
33
34 # The above constraints are *UNSAT* for integer variables.
35 # This reports "no solution"
36 solve(0 < a, 0 < b, a + b < 1, a <= b)
37
38
39
examples/api/python/quickstart.py
1 #!/usr/bin/env python
2 ###############################################################################
3 # Top contributors (to current version):
4 # Yoni Zohar, Aina Niemetz, Alex Ozdemir
5 #
6 # This file is part of the cvc5 project.
7 #
8 # Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
9 # in the top-level source directory and their institutional affiliations.
10 # All rights reserved. See the file COPYING in the top-level source
11 # directory for licensing information.
12 # #############################################################################
13 #
14 # A simple demonstration of the api capabilities of cvc5, adapted from quickstart.cpp
15 ##
16
17 import cvc5
18 from cvc5 import Kind
19
20 if __name__ == "__main__":
21 # Create a solver
22 solver = cvc5.Solver()
23
24 # We will ask the solver to produce models and unsat cores,
25 # hence these options should be turned on.
26 solver.setOption("produce-models", "true");
27 solver.setOption("produce-unsat-cores", "true");
28
29 # The simplest way to set a logic for the solver is to choose "ALL".
30 # This enables all logics in the solver.
31 # Alternatively, "QF_ALL" enables all logics without quantifiers.
32 # To optimize the solver's behavior for a more specific logic,
33 # use the logic name, e.g. "QF_BV" or "QF_AUFBV".
34
35 # Set the logic
36 solver.setLogic("ALL");
37
38 # In this example, we will define constraints over reals and integers.
39 # Hence, we first obtain the corresponding sorts.
40 realSort = solver.getRealSort();
41 intSort = solver.getIntegerSort();
42
43 # x and y will be real variables, while a and b will be integer variables.
44 # Formally, their python type is Term,
45 # and they are called "constants" in SMT jargon:
46 x = solver.mkConst(realSort, "x");
47 y = solver.mkConst(realSort, "y");
48 a = solver.mkConst(intSort, "a");
49 b = solver.mkConst(intSort, "b");
50
51 # Our constraints regarding x and y will be:
52 #
53 # (1) 0 < x
54 # (2) 0 < y
55 # (3) x + y < 1
56 # (4) x <= y
57 #
58
59 # Formally, constraints are also terms. Their sort is Boolean.
60 # We will construct these constraints gradually,
61 # by defining each of their components.
62 # We start with the constant numerals 0 and 1:
63 zero = solver.mkReal(0);
64 one = solver.mkReal(1);
65
66 # Next, we construct the term x + y
67 xPlusY = solver.mkTerm(Kind.ADD, x, y);
68
69 # Now we can define the constraints.
70 # They use the operators +, <=, and <.
71 # In the API, these are denoted by Plus, Leq, and Lt.
72 constraint1 = solver.mkTerm(Kind.LT, zero, x);
73 constraint2 = solver.mkTerm(Kind.LT, zero, y);
74 constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
75 constraint4 = solver.mkTerm(Kind.LEQ, x, y);
76
77 # Now we assert the constraints to the solver.
78 solver.assertFormula(constraint1);
79 solver.assertFormula(constraint2);
80 solver.assertFormula(constraint3);
81 solver.assertFormula(constraint4);
82
83 # Check if the formula is satisfiable, that is,
84 # are there real values for x and y that satisfy all the constraints?
85 r1 = solver.checkSat();
86
87 # The result is either SAT, UNSAT, or UNKNOWN.
88 # In this case, it is SAT.
89 print("expected: sat")
90 print("result: ", r1)
91
92 # We can get the values for x and y that satisfy the constraints.
93 xVal = solver.getValue(x);
94 yVal = solver.getValue(y);
95
96 # It is also possible to get values for compound terms,
97 # even if those did not appear in the original formula.
98 xMinusY = solver.mkTerm(Kind.SUB, x, y);
99 xMinusYVal = solver.getValue(xMinusY);
100
101 # We can now obtain the values as python values
102 xPy = xVal.getRealValue();
103 yPy = yVal.getRealValue();
104 xMinusYPy = xMinusYVal.getRealValue();
105
106 print("value for x: ", xPy)
107 print("value for y: ", yPy)
108 print("value for x - y: ", xMinusYPy)
109
110 # Another way to independently compute the value of x - y would be
111 # to use the python minus operator instead of asking the solver.
112 # However, for more complex terms,
113 # it is easier to let the solver do the evaluation.
114 xMinusYComputed = xPy - yPy;
115 if xMinusYComputed == xMinusYPy:
116 print("computed correctly")
117 else:
118 print("computed incorrectly")
119
120 # Further, we can convert the values to strings
121 xStr = str(xPy);
122 yStr = str(yPy);
123 xMinusYStr = str(xMinusYPy);
124
125
126 # Next, we will check satisfiability of the same formula,
127 # only this time over integer variables a and b.
128
129 # We start by resetting assertions added to the solver.
130 solver.resetAssertions();
131
132 # Next, we assert the same assertions above with integers.
133 # This time, we inline the construction of terms
134 # to the assertion command.
135 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
136 solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
137 solver.assertFormula(
138 solver.mkTerm(
139 Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1)));
140 solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
141
142 # We check whether the revised assertion is satisfiable.
143 r2 = solver.checkSat();
144
145 # This time the formula is unsatisfiable
146 print("expected: unsat")
147 print("result:", r2)
148
149 # We can query the solver for an unsatisfiable core, i.e., a subset
150 # of the assertions that is already unsatisfiable.
151 unsatCore = solver.getUnsatCore();
152 print("unsat core size:", len(unsatCore))
153 print("unsat core:", unsatCore)