diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-22 14:49:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-22 21:49:50 +0000 |
| commit | 0dfbf4b80f25bc9edd1c843ba9a9bb37bace79a9 (patch) | |
| tree | 432a07f4119f031f14c0247982f86f6d76ca9ab0 /test | |
| parent | f1db161860d0283cb5537ad8847e0b52d1485e28 (diff) | |
Fix out-of-sync pruning in CDCAC proofs (#7470)
This PR resolves a subtle issue with CDCAC proofs.
The CDCAC proof is maintained as a tree where (mostly) every node corresponds to an (infeasible) interval generated within the CDCAC method. We prune these intervals regularly to get rid of redundant intervals, which also sorts intervals. The pruning however relied on a stable ordering of both intervals and child nodes within the proof tree, as there was no easy way to map nodes back to intervals.
This PR adds an objectId field to the proof tree nodes and assigns ids to the CDCAC intervals. This allows for a robust mapping between the two, even if the interval list is reordered.
Fixes cvc5/cvc5-projects#313.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress1/nl/factor_agg_s.smt2 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/factor_agg_s.smt2 b/test/regress/regress1/nl/factor_agg_s.smt2 index fd12d4515..fc2e7a789 100644 --- a/test/regress/regress1/nl/factor_agg_s.smt2 +++ b/test/regress/regress1/nl/factor_agg_s.smt2 @@ -3,6 +3,8 @@ ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) +(set-option :check-proofs true) +(set-option :proof-check eager) (declare-fun skoX () Real) (declare-fun skoY () Real) (declare-fun skoZ () Real) |