summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl/stats.h
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2021-04-14 14:50:10 -0300
committerGitHub <noreply@github.com>2021-04-14 17:50:10 +0000
commitb6db4446a28d498af8fb4e629392985dfe2a976c (patch)
treeb283483ce265b25bfdd8e769f2026dd414510ac3 /src/theory/arith/nl/stats.h
parentf74bdbd182d95a8e6395aaaf348ca0e41baa3bf4 (diff)
[unsat-cores] Improving new unsat cores (#6356)
This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly. This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.
Diffstat (limited to 'src/theory/arith/nl/stats.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback