#ifndef GOOSE_ANALYZE_H
#define GOOSE_ANALYZE_H

#include "z3++.h"
#include "llr/llr.h"

namespace goose::analyze
{
    using namespace ir;
    using namespace llr;

    extern z3::context& GetZ3Context();

    extern optional< z3::expr > BuildZ3ExprFromValue( const Value& val );
}

#include "verifstmtvalidator.h"

#endif
