Boogie not support creating new contract

[wmanshu]

Example file: reentry-attack.flint

contract MiniDAO {
  var balances: [Address: Int]
  var total: Wei
}


MiniDAO :: (any) {
  public init()
  mutates (Wei.rawValue)
  {
    self.balances = [:]
    self.total = Wei(0)
  }
}

contract Attacker {
  var stack: Int = 0
  let stackLimit: Int = 10
  var amount: Int
  var dao: MiniDAO
}

Attacker :: caller <- (any) {
  @payable
  public init(implicit value: inout Wei)
  mutates (Wei.rawValue, MiniDAO.total, MiniDAO.balances)
  pre (value.rawValue > 0)
  {
    self.dao = MiniDAO()
    self.amount = value.rawValue
  }

error message:

Error in /home/manshu/Desktop/FromSolidityToFlint:
  Flint to Boogie translation error. Unsupported construct used.
  Details: /tmp/AE0CC45C-0D1F-4AC5-BE37-AF6C2D80BFC3.bpl(617,26): Error: undeclared identifier: nextInstance_MiniDAO
  (Translation Line: 617)
Error in /home/manshu/Desktop/FromSolidityToFlint:
  Flint to Boogie translation error. Unsupported construct used.
  Details: /tmp/AE0CC45C-0D1F-4AC5-BE37-AF6C2D80BFC3.bpl(658,0): Error: wrong number of result variables in call to init_MiniDAO: 1
  (Translation Line: 658)

error happens with self.dao = MiniDAO(), but this contract compiles when skipping the verifier. So I suppose the problem is there isn't a way to translate this line to boogie. ?