cprover
|
SMT Backend. More...
#include "smt2_conv.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/fixedbv.h>
#include <util/format_expr.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/mathematical_expr.h>
#include <util/pointer_offset_size.h>
#include <util/range.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/string2int.h>
#include <util/string_constant.h>
#include <solvers/flattening/boolbv_width.h>
#include <solvers/flattening/c_bit_field_replacement_type.h>
#include <solvers/floatbv/float_bv.h>
#include <solvers/lowering/expr_lowering.h>
#include <solvers/prop/literal_expr.h>
Go to the source code of this file.
Macros | |
#define | UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S); |
#define | SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S) |
SMT Backend.
Definition in file smt2_conv.cpp.
#define SMT2_TODO | ( | S | ) | PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S) |
Definition at line 44 of file smt2_conv.cpp.
#define UNEXPECTEDCASE | ( | S | ) | PRECONDITION_WITH_DIAGNOSTICS(false, S); |
Definition at line 41 of file smt2_conv.cpp.