Marco Gario

@FedericoAureliano thanks for contributing! @mikand I am not clear on the semantics of these operators: - How is floordiv different from div in the integer case? If they do not...

@mikand can we try to take a go/no-go decision about this? My main concern is on the semantics of the operator. Any pointer on this might help.

The main concern with this is the semantics and general applicability across solvers, since there is no smtlib equivalent for this. If you want to move this forward, please make...

:wave: Thanks for reporting this. What is the behavior you expect here? Since the logic is not officially part of the SMT-LIB, we need to understand what to do when...

Thanks for the feedback. I would accept a patch to extend the set of logics to include these cases, if you think you can submit one. In the meanwhile, you...

Benchmarks related to strings: http://stringfuzz.dmitryblotsky.com/suites/generated/

If you are up to work on this, that would be awesome! I did the simple part of the simplification (i.e., no simplification), and I am missing the more interesting...

I should have a sometime in the next few days to get through this.

> As for note2: do you think that this could be handled in the equality conversion? > For example, we could add a line saying that if both the arguments...

Tests are missing. After doing the change that @mikand suggested, the test cases should include the ones that already exist for Z3 and MathSAT. Please, double check that they are...