Márk Somorjai

This is the result of my BSc degree project: a CHC frontend implemented in Theta. It can be enabled with the `--chc` flag, and different transformation methods can be chosen...

Putting the general versions of variables into the precision instead of the instance versions makes Theta not be able to verify some tasks, while allowing some previously unverified tasks to...

Log level affects Z3 behavior

1

Running Theta in different log level configurations leads to `Z3Exception` for certain log levels, while resulting in successful verification for others. **Theta version:** [b56a6ac](https://github.com/s0mark/theta/tree/b56a6ac0b046c320d06a6c3f996def849e89864a) **Input task:** [recursive-simple/id2_b3_o2.c](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/recursive-simple/id2_b3_o2.c?ref_type=heads) **Configuration:** `--domain PRED_CART...