As far as I understand, their approach is exactly that, i.e., another target language for extraction. Synthesis is a bit of an overloaded term.
domain(100..999).
digit(0..9).
% Variation w/ prime factors
prime(P) :- domain(P), { domain(F) : F < P, P \ F == 0 } 0.
prod(P1 * P2) :- prime(P1;P2).
% Palindrome
pd(X) :- prod(X), X = 100000*A + 10000*B + 1000*C + 100*C + 10*B + A,
digit(A;B;C).
pdMax(M) :- M = #max { X : pd(X) }.
#show pdMax/1.
Superficially it resembles Prolog, but brings "true" declarativity to the table, i.e., the order of rules and the order of atoms in the body is negligible. Various notions of safety and the prohibition of nested complex terms (e.g. `f(f(x))') guarantee termination. Most importantly though, solutions to an answer set program are not proofs (as in Prolog) but truth-assignments of atoms ("answer sets"). In this specific encoding there's no significant difference though, as we're only computing a single answer set containing an atom "pdMax(X)" with the maximum palindrome X.