Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80 stars 17 forks source link

Add the String theory to the `ALL` logic of SMT-LIB #182

Closed hra687261 closed 1 year ago

hra687261 commented 1 year ago

The added test didn't pass before, not sure if there are other necessary changes, but this seems to fix the issue.

Gbury commented 1 year ago

The fix is good indeed, but a more accurate description would be: "add the String theory to the ALL logic of smtlib". I'm not sure the test is needed (it's unlikely for the string theory to disappear and cause a regression).

hra687261 commented 1 year ago

Alright, removed it.