ยง Presburger arithmetic can represent the Collatz Conjecture

An observation I had: the function 
f(x) = x/2      if (x % 2 == 0)
f(x) = 3x + 1   otherwise
is a Presburger function, so by building better approximations to the transitive closure of a presburger function, one could get better answers to the Collatz conjecture. Unfortunately, ISL (the integer set library) of today is not great against the formidable foe. The code: 
#include <isl/set.h>
#include <isl/version.h>
#include <isl/map.h>
#include <isl/aff.h>
#include <isl/local_space.h>
#include <isl/constraint.h>
#include <isl/space.h>

int main() {
    isl_ctx *ctx = isl_ctx_alloc();
    const char *s = "{ [x] -> [x / 2] : x >= 1 and x % 2 = 0; [x] -> [3 * x + 1] : x % 2 = 1}";

    isl_map *m = isl_map_read_from_str(ctx, s);

    isl_map_dump(m);

    int b = 0;
    isl_map *p = isl_map_transitive_closure(m, &b);
    p = isl_map_coalesce(p);
    printf("exact: %d\n", b);
    printf("map:\n");
    isl_map_dump(p);
    printf("map's range:\n");
    isl_set_dump(isl_set_coalesce(isl_map_range(isl_map_copy(p))));
    // print("map's range intersect 1: %d\n");


}
Produces the somewhat disappointing, and yet expected output: 
$ g++ isl.c -lisl -Lisl-0.20/.libs -o isl -I/usr/local/include/ && ./isl
{ [x] -> [o0] : (2o0 = x and x > 0) or (exists (e0 = floor((1 + x)/2): o0 = 1 + 3x and 2e0 = 1 + x)) }
exact: 0
map:
{ [x] -> [o0] : (o0 < x and o0 > 0) or (exists (e0 = floor((x)/2), e1 = floor((2 + o0)/6), e2, e3, e4 = floor((-x + o0 + e2 - e3)/4): 2e0 = x and 6e1 = 2 + o0 and x >= 2 and 4e4 >= -3 - x + o0 + e2 - e3 and 4e4 >= 4 - x + o0 - 2e2 + 2e3 and 4e4 <= -x + o0 + e2 - e3)) or (exists (e0 = floor((x)/2), e1, e2, e3 = floor((-x + o0 + e1 - e2)/4): 2e0 = -1 + x and o0 > 0 and 4e3 >= -3 - x + o0 + e1 - e2 and 4e3 >= 3 - x + o0 - 2e1 + 2e2 and 4e3 <= -x + o0 + e1 - e2)) or (exists (e0 = floor((x)/2), e1, e2, e3 = floor((-x + o0 + e1 - e2)/4): 2e0 = x and x >= 2 and o0 > 0 and 4e3 >= -3 - x + o0 + e1 - e2 and 4e3 >= 3 - x + o0 - 2e1 + 2e2 and 4e3 <= -x + o0 + e1 - e2)) or (exists (e0 = floor((x)/2), e1 = floor((2 + o0)/6): 2e0 = -1 + x and 6e1 = 2 + o0 and o0 < x)) or (exists (e0 = floor((x)/2), e1 = floor((2 + o0)/6): 2e0 = x and 6e1 = 2 + o0 and x >= 2 and o0 <= -2 + x)) or (exists (e0 = floor((x)/2), e1 = floor((2 + o0)/6), e2, e3, e4 = floor((-x + o0 + e2 - e3)/4): 2e0 = -1 + x and 6e1 = 2 + o0 and 4e4 >= -3 - x + o0 + e2 - e3 and 4e4 >= 3 - x + o0 - 2e2 + 2e3 and 4e4 <= -x + o0 + e2 - e3)) }
map's range:
{ [i0] : i0 > 0 or exists (e0 = floor((2 + i0)/6): 6e0 = 2 + i0) }
I've yet to check that the image contains a 1 for every choice of x.