add no except
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -76,7 +76,7 @@ static bool is_power2(const expr &e, unsigned &log) {
namespace smt {
-expr::expr(Z3_ast ast) : ptr((uintptr_t)ast) {
+expr::expr(Z3_ast ast) noexcept : ptr((uintptr_t)ast) {
static_assert(sizeof(Z3_ast) == sizeof(uintptr_t));
assert(isZ3Ast() && isValid());
incRef();
@@ -100,7 +100,7 @@ Z3_ast expr::ast() const {
return 0;
}
-expr::expr(const expr &other) {
+expr::expr(const expr &other) noexcept {
if (!other.isValid()) {
ptr = 0;
} else if (other.isZ3Ast()) {
@@ -111,7 +111,7 @@ expr::expr(const expr &other) {
}
}
-expr::~expr() {
+expr::~expr() noexcept {
if (isValid()) {
if (isZ3Ast()) {
decRef();

MODIFY
smt/expr.h
smt/expr.h
@@ -23,7 +23,7 @@ namespace smt {
class expr {
uintptr_t ptr;
- expr(Z3_ast ast);
+ expr(Z3_ast ast) noexcept;
bool isZ3Ast() const;
Z3_ast ast() const;
Z3_ast operator()() const { return ast(); }
@@ -67,9 +67,9 @@ public:
std::swap(ptr, other.ptr);
}
- expr(const expr &other);
- expr(bool val) : expr(val ? mkTrue() : mkFalse()) {}
- ~expr();
+ expr(const expr &other) noexcept;
+ expr(bool val) noexcept : expr(val ? mkTrue() : mkFalse()) {}
+ ~expr() noexcept;
void operator=(expr &&other);
void operator=(const expr &other);

MODIFY
util/unionfind.cpp
util/unionfind.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "util/unionfind.h"
-#include <vector>
using namespace std;

add no except