void addConstInterp(FuncDecl decl, Expr value) { _c._z3.add_const_interp( _model, _c._createFuncDecl(decl), _c._createAST(value), ); }