Skip to content

Make it possible to enable/disable theories (and load their preludes or not) using the set-option command in SMT-LIB files#1363

Open
hra687261 wants to merge 3 commits into
OCamlPro:nextfrom
hra687261:set-option-theories
Open

Make it possible to enable/disable theories (and load their preludes or not) using the set-option command in SMT-LIB files#1363
hra687261 wants to merge 3 commits into
OCamlPro:nextfrom
hra687261:set-option-theories

Conversation

@hra687261

Copy link
Copy Markdown
Contributor

I wrote this code initially while working on #1358 (to be able to run tests in which different theories are enabled/disabled in the smt-lib file) but I thought it might be useful to upstream it, though the changes to solving_loop.ml ended being bigger than initially intended, and I am not sure if this feature is worth complicating the code this much.

@hra687261 hra687261 force-pushed the set-option-theories branch from 6102b03 to 846039c Compare June 18, 2026 15:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant