        void operator-=(variable_t var) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }

        interval_t operator[](variable_t v) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }

        void set(variable_t v, interval_t ival) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }

        void operator += (linear_constraint_system_t csts) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        void assign (variable_t x, linear_expression_t e) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
          
        void apply (operation_t op, variable_t x, variable_t y, Number z) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        void apply(operation_t op, variable_t x, variable_t y, variable_t z) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        void apply(operation_t op, variable_t x, Number k) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }

        void apply(int_conv_operation_t op, variable_t dst, variable_t src) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
	
        void apply(bitwise_operation_t op, variable_t x, variable_t y, variable_t z) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        void apply(bitwise_operation_t op, variable_t x, variable_t y, Number k) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        void apply(div_operation_t op, variable_t x, variable_t y, variable_t z) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        void apply(div_operation_t op, variable_t x, variable_t y, Number k) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        void backward_assign (variable_t x, linear_expression_t e,
			      elina_domain_t invariant) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
          
        void backward_apply (operation_t op,
			     variable_t x, variable_t y, Number z,
			     elina_domain_t invariant) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        void backward_apply(operation_t op,
			    variable_t x, variable_t y, variable_t z,
			    elina_domain_t invariant) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
        
        linear_constraint_system_t to_linear_constraint_system ()
        { CRAB_ERROR(ELINA_NOT_FOUND); }

        disjunctive_linear_constraint_system_t to_disjunctive_linear_constraint_system ()
        { CRAB_ERROR(ELINA_NOT_FOUND); }
	
        void write(crab_os& o) 
        { CRAB_ERROR(ELINA_NOT_FOUND); }
          
        static std::string getDomainName () {
          return "Dummy Elina";
        }  
      }; 
   } // namespace domains
}// namespace crab
#else

/* 
 * Real implementation starts here.
 * The code is a copy-and-paste version of apron_domains.hpp.
 * Thanks to <NAME>. 
 */

#include <crab/domains/elina/elina.hpp>
#include <boost/bimap.hpp>
#include <crab/domains/linear_interval_solver.hpp>

namespace crab {
namespace domains {
  
  using namespace elina;

  template<typename Number, typename VariableName, elina_domain_id_t ElinaDom>
  class elina_domain_:
    public abstract_domain<Number,VariableName,
			   elina_domain_<Number,VariableName,ElinaDom> > {
    
    typedef elina_domain_<Number, VariableName, ElinaDom> elina_domain_t;
    typedef abstract_domain<Number,VariableName,elina_domain_t> abstract_domain_t;
  public:
    using typename abstract_domain_t::linear_expression_t;
    using typename abstract_domain_t::linear_constraint_t;
    using typename abstract_domain_t::linear_constraint_system_t;
    using typename abstract_domain_t::disjunctive_linear_constraint_system_t;    
    using typename abstract_domain_t::variable_t;
    using typename abstract_domain_t::number_t;
    using typename abstract_domain_t::varname_t;
    using typename abstract_domain_t::variable_vector_t;	
    typedef interval <Number> interval_t;
    
  private:
    typedef interval_domain <Number, VariableName> interval_domain_t;
    typedef bound <Number> bound_t;
    typedef boost::bimap<variable_t, elina_dim_t > var_map_t;
    typedef typename var_map_t::value_type binding_t;
    
    static elina_manager_t* m_apman;
    
    elina_state_ptr m_apstate; 
    var_map_t m_var_map;
    
    static elina_manager_t* get_man () {
      if (!m_apman) {
	switch (ElinaDom) {
	case ELINA_ZONES: m_apman = opt_zones_manager_alloc(); break;
	case ELINA_OCT: m_apman = opt_oct_manager_alloc(); break;
	case ELINA_PK : m_apman = opt_pk_manager_alloc(false); break;
	default: CRAB_ERROR("unknown elina domain");
	}
      }
      return m_apman;
    }
    
    size_t get_dims (elina_state_ptr s) const {
      elina_dimension_t dims = _elina_abstract0_dimension (&*s);
      return dims.intdim;
    }
    
    size_t get_dims () const { return get_dims (m_apstate); }
    
    // If v is in the map then it maps v to a dimension, otherwise null
    boost::optional<elina_dim_t> get_var_dim (const var_map_t& m, variable_t v) const {
      auto it = m.left.find (v);
      if (it!= m.left.end ())
	return it->second;
      else
	return boost::optional<elina_dim_t> ();
    }
    
    boost::optional<elina_dim_t> get_var_dim (variable_t v) const {
      return get_var_dim (m_var_map, v);
    }
    
    elina_dim_t get_var_dim_insert (variable_t v) {
      assert (m_var_map.size () == get_dims ());
      if (auto dim = get_var_dim (v))
	return *dim;
      else {
	elina_dim_t i = m_var_map.size ();
	m_var_map.insert (binding_t (v, i));
	add_dimensions (m_apstate, 1);
	assert (m_var_map.size () == get_dims ());
	return i;
      }
    }
    
    bool has_variable (const var_map_t& m, elina_dim_t i) const {
      return m.right.find (i)!= m.right.end ();
    }
    
    bool has_variable (elina_dim_t i) const {
      return has_variable (m_var_map, i);
    }
    
    variable_t get_variable (const var_map_t& m, elina_dim_t i) const {
      auto it = m.right.find (i);
      if (it!= m.right.end ())
	return it->second;            
      CRAB_ERROR("Elina dimension ", i, " is not used!");
    }
    
    variable_t get_variable (elina_dim_t i) const {
      return get_variable (m_var_map, i);
    }
    
    