There are several distinct algorithmic problems that you are referring to.
First of all, we can consider decision problems for finitely presented groups with solvable word problem given by finite presentations.
In this case, we only consider groups that have solvable word problem, but the input to the decision problems we are interested in remain finite presentations.
The Boone-Rogers theorem says that the word problem is not uniformly solvable on the set of groups that have solvable word problem: this means that the assumption that we are dealing with groups that have solvable word problem cannot be used.
And in this case, Markov properties of groups with solvable word problem remain undecidable.
Boone-Rogers-Adian-Rabin Theorem: Let $P$ be a Markov property of groups with solvable word problem : there exists a finitely presented group with solvable word problem that has this property and a finitely presented group with solvable word problem that does not embed in a group with solvable word problem that has $P$.
Then there is no algorithm that, on input a finite presentation of a group with solvable word problem, can decide whether or not this group has $P$.
Proof:
Let $G_+$ and $G_-$ be the positive and negative witnesses.
Miller's version of the Adian-Rabin construction (see here, Lemma 3.6) does the following. On input a finite presentation $\pi=\langle S \vert R \rangle$ and a word $w\in(S\cup S^{-1})^*$, it provides a finite presentation $\Pi_{\pi,w}$ such that $\Pi_{\pi,w}$ is isomorphic to $G_+$ iff $w=1$ in the group defined by $\pi$, and $\Pi_{\pi,w}$ contains $G_-$ iff $w\neq1$ in the group defined by $\pi$.
For the usual Adian-Rabin Theorem, you conclude by choosing a single $\pi$ that defines a group with unsolvable word problem, and having $w$ vary.
In the present case, we consider instead a sequence of finite presentations $\pi_n$, $n\in\mathbb{N}$, together with a sequence of words $w_n$ such that: each $\pi_n$ defines a group with solvable word problem, but no algorithm can, on input $n\in\mathbb{N}$, decide whether $w_n=1$ in $\pi_n$. This sequence is precisely what is given by the Boone-Rogers Theorem.
A second possibility is to, again, consider finitely presented groups with solvable word problem, but now to consider decision problems where groups are given by both a finite presentation and by a solution to the word problem. (When a group has solvable word problem, the algorithm that solves the word problem in it consists in finite data, and it can be given as input to other programs, as in the Universal Turing Machine theorem.)
This is a very interesting research topic, started by Daniel Groves and Henry Wilton, see the references given by Henry in the comments.
In this case, the notion of "Markov property" becomes less relevant, and some Markov properties are decidable (being trivial, being abelian, being free), while others are still undecidable, like being torsion free. To prove that being torsion free is undecidable even when we have access to a solution to the word problem, we can use the fact that the version of the Higman embedding theorem that preserves solvability of the word problem (Higman-Clapham-Valiev Theorem) also preserves torsion freeness (as remarked by Lempp). Then the easy fact that being torsion-free is undecidable for groups given by word problem algorithms (a result of Lockhart about groups that need not be finitely presented) transfers directly to the present setting.
A last notion one may want to consider (and alluded to by the op) is to consider groups given by finitely presentations and whose solution to the word problem is given by an oracle. (So in one case the solution to the word problem is given by the code of a machine that solves it, it the other case by an oracle, which is just an infinite tape where the trivial words of your groups are all written in shortlex order.)
I expect that this will give a notion of computable function equivalent to the previous one, but it is an open problem to show this.
This is an instance of the "continuity problem", studied in computable analysis. For instance the Kreisel-Lacombe-Schoenfield-Tseitin Theorem establishes such an equivalence on the Baire space.
