smt2_conv.cpp File Reference

SMT Backend. More...

#include "smt2_conv.h"
#include <util/arith_tools.h>
#include <util/base_type.h>
#include <util/c_types.h>
#include <util/config.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/pointer_offset_size.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 dependency graph for smt2_conv.cpp:

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)

Detailed Description

SMT Backend.

Definition in file smt2_conv.cpp.

Macro Definition Documentation

SMT2_TODO

#define SMT2_TODO

(

S

)

PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)

Definition at line 41 of file smt2_conv.cpp.

UNEXPECTEDCASE

#define UNEXPECTEDCASE

(

S

)

PRECONDITION_WITH_DIAGNOSTICS(false, S);

Definition at line 38 of file smt2_conv.cpp.