Goose  Diff

    class Builder;

    extern z3::context& GetZ3Context();
    extern optional< z3::expr > BuildZ3ExprFromValue( Builder& b, const Value& val );
    extern optional< z3::expr > BuildZ3ConstantFromType( const Term& type, const string& name );
    extern optional< z3::expr > BuildZ3Op( Builder& b, const llr::Instruction& instr );

    class Z3SolverStateGuard
    {
        public:
            Z3SolverStateGuard( z3::solver& s ) :
                m_solver( s )
            {
                s.push();
            }

            ~Z3SolverStateGuard()
            {
                m_solver.pop();
            }

        private:
            z3::solver& m_solver;
    };
}

#include "remapper.h"
#include "builder.h"
#include "condition.h"
#include "func.h"