diff --git a/README.md b/README.md
index 3444618..4326b72 100644
--- a/README.md
+++ b/README.md
@@ -48,7 +48,14 @@ python3 satuio/ads-core.py --help
 
 The solver can be specified (as long as pysat supports it). The default is
 [Glucose3](https://www.labri.fr/perso/lsimon/glucose/), as that worked
-well on the examples.
+well on the examples. After a bit more testing, these work well: `g3`, `mc`,
+`m22`. These are okay: `gc3`, `gc4`, `g4`, `mgh`. And these were slow for me:
+`cd`, `lgl`, `mcb`, `mcm`, `mpl`, `mg3`.
+
+The encoding currectly defaults to `seqcounter` for cardinality constraints.
+This seems to work just fine, and I am not even sure the encodings are really
+different for cardinality of `k=1`. It could be worth doing more testing to
+see which is the fastest.
 
 
 ## Copyright
diff --git a/satuio/ads-core.py b/satuio/ads-core.py
index 82be28e..97449ef 100644
--- a/satuio/ads-core.py
+++ b/satuio/ads-core.py
@@ -1,7 +1,8 @@
 """
 WIP script for returning the unsat core in the case an ADS does
 *not* exist. This could be merged into the main ads script,
-although there is an additional cost (presumably). Usage:
+although there is an additional cost (presumably). For now, this
+is mostyl copy-pasted from ads.py. Usage:
 
   python3 ads-core.py --help
 
@@ -21,6 +22,10 @@ from utils.parser import read_machine
 from utils.utils import *
 
 
+# We set up some things for nice output
+console = Console(highlight=False)
+
+
 # *****************
 # Reading the input
 # *****************
@@ -41,7 +46,7 @@ if args.states == None or len(args.states) <= 1:
 states = args.states
 length = args.length
 
-measure_time('Constructed automaton with', len(all_states), 'states and', len(alphabet), 'symbols')
+console.print(now(), f'Constructed automaton with [bold blue]{len(all_states)} states[/bold blue], [bold green]{len(alphabet)} symbols[/bold green] and Q_0 has [bold blue]{len(states)} states[/bold blue]')
 
 
 # ********************
@@ -100,7 +105,7 @@ def unique(lits):
   cnf = CardEnc.equals(lits, 1, vpool=vpool, encoding=EncType.seqcounter)
   solver.append_formula(cnf.clauses)
 
-measure_time('Setup solver', args.solver)
+console.print(now(), f'Solver {args.solver} ready for clauses')
 
 
 # ********************
@@ -114,7 +119,7 @@ measure_time('Setup solver', args.solver)
 # used to decide whether we found a different output.
 possible_outputs = {}
 possible_states = {}
-for s in tqdm(states, desc="CNF paths"):
+for s in tqdm(states, desc="CNF paths", leave=False):
   # current set of possible states we're in
   current_set = set([s])
   # set of successors for the next iteration of i
@@ -162,7 +167,7 @@ for s in tqdm(states, desc="CNF paths"):
 
 # Now we will encode differences in outputs (and equal inputs, as
 # long as there is no difference).
-for s in tqdm(states, desc="CNF diffs"):
+for s in tqdm(states, desc="CNF diffs", leave=False):
   for t in states:
     # We skip s == t, since those state are equivalent.
     # I am not sure whether we can skip s <= t, since our construction
@@ -231,7 +236,7 @@ for s in tqdm(states, desc="CNF diffs"):
           solver.add_clause(enable_for_core + [-dvar(s, t, i), -ovar(s, i, o), -ovar(t, i, o)])
 
 
-measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver.nof_vars(), 'variables')
+console.print(now(), f'Constructed CNF with {solver.nof_clauses()} clauses and {solver.nof_vars()} variables')
 
 
 # ******************
@@ -239,7 +244,6 @@ measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver
 # ******************
 
 # We set up some things for nice output
-console = Console(markup=False, highlight=False)
 max_state_length = max([len(str) for str in states])
 
 # Solve it!
@@ -249,17 +253,17 @@ solution = False
 while current_states and not solution:
   enabled_states = [evar(s) for s in current_states]
   solution = solver.solve(assumptions=enabled_states)
-  measure_time('Solver finished')
+  console.print(now(), 'Solver finished')
 
   # If there is no solution, we can exit. As far as I know
   # there is no relevant information in the "core", as there
   # are no assumptions used in our encoding.
   if solution:
-    console.print('! ADS of length', length, 'for', len(current_states), 'states exists', style='bold green')
-    measure_total_time('Done')
+    console.print(f'! ADS of length {length} for {len(current_states)} states exists', style='bold green')
+    console.print(now(), 'Done')
     exit()
 
-  console.print('! no ADS of length', length, 'for', len(current_states), 'states', style='bold red')
+  console.print(f'! no ADS of length {length} for {len(current_states)} states', style='bold red')
 
   core = solver.get_core()
   core_set = set()
@@ -269,11 +273,11 @@ while current_states and not solution:
 
   core_states = [s for s in states if evar(s) in core_set]
   fine_states = [s for s in states if evar(s) not in core_set]
-  print(len(core_states), 'states in the unsat core')
-  print('core states =', core_states)
-  print('fine states =', fine_states)
+  console.print(f'{len(core_states)} states in the unsat core')
+  console.print(f'core states = {core_states}')
+  console.print(f'fine states = {fine_states}')
 
   current_states = fine_states
 
 
-measure_total_time('Done')
+console.print(now(), 'Done')
diff --git a/satuio/ads.py b/satuio/ads.py
index 41648bc..dd47c49 100644
--- a/satuio/ads.py
+++ b/satuio/ads.py
@@ -26,6 +26,11 @@ from tqdm import tqdm               # Import fancy progress bars
 
 from utils.parser import read_machine
 from utils.utils import *
+import random
+
+
+# We set up some things for nice output
+console = Console(highlight=False)
 
 
 # *****************
@@ -38,19 +43,25 @@ parser.add_argument('filename', help='File of the mealy machine (dot format)')
 parser.add_argument('length', help='Length of the ADS', type=int)
 parser.add_argument('-v', '--verbose', help='Show more output', action='store_true')
 parser.add_argument('--show-differences', help='Show even more output', action='store_true')
+parser.add_argument('--random-base', help='Chooses a random base', action='store_true')
+parser.add_argument('--base-size', type=int)
 parser.add_argument('--solver', help='Which solver to use (default g3)', default='g3')
 parser.add_argument('--states', help='For which states to compute an ADS', nargs='+')
 args = parser.parse_args()
 
-if args.states == None or len(args.states) <= 1:
-  raise ValueError('Should specify at least 2 states')
-
 # reading the automaton
 (alphabet, outputs, all_states, delta, labda) = read_machine(args.filename)
 states = args.states
 length = args.length
 
-measure_time('Constructed automaton with', len(all_states), 'states and', len(alphabet), 'symbols')
+if args.random_base and args.base_size > 1:
+  states = random.sample(all_states, k=args.base_size)
+elif len(args.states) > 1:
+  states = args.states
+else:
+  raise ValueError('Should specify at least 2 states')
+
+console.print(now(), f'Constructed automaton with [bold blue]{len(all_states)} states[/bold blue], [bold green]{len(alphabet)} symbols[/bold green] and Q_0 has [bold blue]{len(states)} states[/bold blue]')
 
 
 # ********************
@@ -102,7 +113,7 @@ def unique(lits):
   cnf = CardEnc.equals(lits, 1, vpool=vpool, encoding=EncType.seqcounter)
   solver.append_formula(cnf.clauses)
 
-measure_time('Setup solver', args.solver)
+console.print(now(), f'Solver {args.solver} ready for clauses')
 
 
 # ********************
@@ -116,7 +127,7 @@ measure_time('Setup solver', args.solver)
 # used to decide whether we found a different output.
 possible_outputs = {}
 possible_states = {}
-for s in tqdm(states, desc="CNF paths"):
+for s in tqdm(states, desc="CNF paths", leave=False):
   # current set of possible states we're in
   current_set = set([s])
   # set of successors for the next iteration of i
@@ -164,7 +175,7 @@ for s in tqdm(states, desc="CNF paths"):
 
 # Now we will encode differences in outputs (and equal inputs, as
 # long as there is no difference).
-for s in tqdm(states, desc="CNF diffs"):
+for s in tqdm(states, desc="CNF diffs", leave=False):
   for t in states:
     # We skip s == t, since those state are equivalent.
     # I am not sure whether we can skip s <= t, since our construction
@@ -230,7 +241,7 @@ for s in tqdm(states, desc="CNF diffs"):
           solver.add_clause([-dvar(s, t, i), -ovar(s, i, o), -ovar(t, i, o)])
 
 
-measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver.nof_vars(), 'variables')
+console.print(now(), f'Constructed CNF with {solver.nof_clauses()} clauses and {solver.nof_vars()} variables')
 
 
 # ******************
@@ -238,19 +249,18 @@ measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver
 # ******************
 
 # We set up some things for nice output
-console = Console(markup=False, highlight=False)
 max_state_length = max([len(str) for str in states])
 
 # Solve it!
 solution = solver.solve()
-measure_time('Solver finished')
+console.print(now(), 'Solver finished')
 
 # If there is no solution, we can exit. As far as I know
 # there is no relevant information in the "core", as there
 # are no assumptions used in our encoding.
 if not solution:
   console.print('! no ADS of length', length, style='bold red')
-  measure_total_time('Done')
+  console.print(now(), 'Done')
   exit()
 
 # Get the set of true variables
@@ -351,17 +361,14 @@ def extract_tree(initial_set, level):
 def print_tree(console, tree, left=''):
   # The leaf is inlined in the printing
   if 'leaf' in tree:
-    console.print('> state', end=' ')
-    console.print(tree['leaf'], style='bold blue')
+    console.print(f'> state [bold blue]{tree["leaf"]}[/bold blue]')
   else:
     # The next input symbol is also inlined
-    console.print('> ', end='')
-    console.print(tree['split_symbol'], end='', style='bold green')
+    console.print(f'> [bold green]{tree["split_symbol"]}[/bold green]', end='')
     # We contract single-successor paths in the tree
     while len(tree['subtree']) == 1:
       tree = some_elem(tree['subtree'].values())
-      console.print(' - ', end='')
-      console.print(tree['split_symbol'], end='', style='bold green')
+      console.print(f' - [bold green]{tree["split_symbol"]}[/bold green]', end='')
     else:
       console.print()
       counter = len(tree['subtree'])
@@ -381,7 +388,7 @@ print_tree(console, extract_tree(states, 0))
 print('')
 
 # Report some final stats
-measure_total_time('Done')
+console.print(now(), 'Done')
 
 
 # TODO: we know that dvar(s, t, i) is an equivalence relation for
diff --git a/satuio/uio-incr.py b/satuio/uio-incr.py
index 8b40410..4655db0 100644
--- a/satuio/uio-incr.py
+++ b/satuio/uio-incr.py
@@ -44,6 +44,7 @@ parser.add_argument('--time', help='Upper bound on search time (ms)', type=int)
 parser.add_argument('--solver', help='Which solver to use (default g3)', default='g3')
 parser.add_argument('--bases', help='For which states to compute an UIO (leave empty for all states)', nargs='*')
 parser.add_argument('--log', help='Enable the additional log file', action='store_true')
+parser.add_argument('-v', '--verbose', help='Show more output', action='store_true')
 args = parser.parse_args()
 
 # reading the automaton
@@ -255,7 +256,7 @@ while True:
     # and we also record the outputs along this path. The outputs are later
     # used to decide whether we found a different output.
     possible_outputs = {}
-    for s in tqdm(states, desc="CNF paths", leave=False):
+    for s in tqdm(states, desc="CNF paths", leave=args.verbose):
       # current set of possible states we're in
       current_set = set([s])
       # set of successors for the next iteration of i
@@ -307,7 +308,7 @@ while True:
     # Also note, we only encode the converse: if there is a difference claimed
     # and base has a certain output, than the state should not have that output.
     # This means that the solver doesn't report all differences, but at least one.
-    for s in tqdm(states, desc="CNF diffs", leave=False):
+    for s in tqdm(states, desc="CNF diffs", leave=args.verbose):
       # Constraint: there is a place, such that there is a difference in output
       # \/_i x_('e', s, i)
       # If s is our base, we don't care (this can be done, because only
@@ -347,7 +348,7 @@ while True:
     # We want to find an UIO for each base. We have already constructed
     # the CNF. So it remains to add assumptions to the solver, this is
     # called "incremental solving" in SAT literature.
-    for base in tqdm(bases, desc='solving', leave=False):
+    for base in tqdm(bases, desc='solving', leave=args.verbose):
       # If we run out of time, stop solving (but finish other stuff)
       if args.time and time_since_start() * 1000 > args.time:
         break
@@ -393,7 +394,7 @@ for (s, uio) in uios.items():
 console.print('')
 
 # Report some final stats
-measure_total_time('\nDone')
+console.print(now(), 'Done')
 console.print(f'uios found: {100*len(uios)/len(states):.0f}%')
 console.print(f'avg length: {sum([len(uio) for uio in uios.values()])/len(uios):.3}')
 
diff --git a/satuio/uio.py b/satuio/uio.py
index 84477af..b350ef9 100644
--- a/satuio/uio.py
+++ b/satuio/uio.py
@@ -23,6 +23,10 @@ from utils.parser import read_machine
 from utils.utils import *
 
 
+# We set up some things for nice output
+console = Console(highlight=False)
+
+
 # *****************
 # Reading the input
 # *****************
@@ -47,7 +51,7 @@ else:
 
 length = args.length
 
-measure_time('Constructed automaton with', len(states), 'states and', len(alphabet), 'symbols')
+console.print(now(), f'Constructed automaton with {len(states)} states and {len(alphabet)} symbols')
 
 
 # ********************
@@ -104,7 +108,7 @@ def unique(lits):
   cnf = CardEnc.equals(lits, 1, vpool=vpool, encoding=EncType.seqcounter)
   solver.append_formula(cnf.clauses)
 
-measure_time('Setup solver', args.solver)
+console.print(now(), 'Setup solver', args.solver)
 
 
 # ********************
@@ -125,7 +129,7 @@ unique([bvar(base) for base in bases])
 # and we also record the outputs along this path. The outputs are later
 # used to decide whether we found a different output.
 possible_outputs = {}
-for s in tqdm(states, desc="CNF paths"):
+for s in tqdm(states, desc="CNF paths", leave=args.verbose):
   # current set of possible states we're in
   current_set = set([s])
   # set of successors for the next iteration of i
@@ -177,7 +181,7 @@ for s in tqdm(states, desc="CNF paths"):
 # Also note, we only encode the converse: if there is a difference claimed
 # and base has a certain output, than the state should not have that output.
 # This means that the solver doesn't report all differences, but at least one.
-for s in tqdm(states, desc="CNF diffs"):
+for s in tqdm(states, desc="CNF diffs", leave=args.verbose):
   # Constraint: there is a place, such that there is a difference in output
   # \/_i x_('e', s, i)
   # If s is our base, we don't care (this can be done, because only
@@ -207,7 +211,7 @@ for s in tqdm(states, desc="CNF diffs"):
         if o in outputs_s:
           solver.add_clause([-bv, -evar(s, i), -ovar(base, i, o), -ovar(s, i, o)])
 
-measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver.nof_vars(), 'variables')
+console.print(now(), f'Constructed CNF with {solver.nof_clauses()} clauses and {solver.nof_vars()} variables')
 
 
 # ******************
@@ -215,7 +219,6 @@ measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver
 # ******************
 
 # We set up some things for nice output
-console = Console(markup=False, highlight=False)
 max_state_length = max([len(str) for str in states])
 
 # We count the number of uios
@@ -225,20 +228,17 @@ num_uios = {True: 0, False: 0}
 # the CNF. So it remains to add assumptions to the solver, this is
 # called "incremental solving" in SAT literature.
 for base in bases:
-  console.print('')
-  console.print('*** UIO for state', base, style='bold blue')
-
   # Solve with bvar(base) being true
   b = solver.solve(assumptions=[bvar(base)])
   num_uios[b] = num_uios[b] + 1
-  measure_time('Solver finished')
+  console.print(now(), f'Solved for [bold blue]{base}[/bold blue]')
 
   if b:
     # Get the set of true variables
     truth = get_truth(solver)
 
     # We print the word
-    console.print('! UIO of length', length, style='bold green')
+    console.print(f'       UIO of length {length}: ', end='')
     for i in range(length):
       for a in alphabet:
         if avar(i, a) in truth:
@@ -269,13 +269,13 @@ for base in bases:
         console.print('')
 
   else:
-    console.print('! no UIO of length', length, style='bold red')
+    console.print(f'       no UIO of length {length}', style='bold red')
     # The core returned by the solver is not interesting:
     # It is only the assumption (i.e. bvar).
 
 print('')
 
 # Report some final stats
-measure_total_time('\nDone')
-print('With UIO:', num_uios[True])
-print('without: ', num_uios[False])
+console.print(now(), 'Done')
+console.print('With UIO:', num_uios[True])
+console.print('without: ', num_uios[False])
diff --git a/satuio/utils/utils.py b/satuio/utils/utils.py
index 0733a73..47f7daa 100644
--- a/satuio/utils/utils.py
+++ b/satuio/utils/utils.py
@@ -13,17 +13,6 @@ from time import time
 start = time()
 start_total = start
 
-def measure_time(*str):
-  global start
-  now = time()
-  print('***', *str, "in %.3f seconds" % (now - start))
-  start = now
-
-def measure_total_time(*str):
-  global start_total
-  now = time()
-  print('***', *str, ": total time = %.3f seconds" % (now - start_total))
-
 def time_since_start():
   return time() - start_total