We present a novel language-agnostic approach to test case generation from a logic program representation generated by an existing framework. This is nontrivial for two reasons: since in such representation basic statements are usually composed into complex formulas, the trace enumerator cannot distill statements that are yet to be covered, and since the formulas obtained this way are more complex, the satisfiability checks are costlier and their number has to be kept low. Our approach performs an accelerated trace enumeration exploiting the program structure on the go. Our new implementation on top of the Horntinuum test case generator calls an SMT solver incrementally to achieve a significant performance increase. Furthermore, it has found many new test cases in public benchmarks that state-of-the-art did not find.