diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-25 13:23:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-25 18:23:39 +0000 |
| commit | 50da62ab1ebd71d619e4ada901c35009396f772e (patch) | |
| tree | 6a1df78ab66d53c40621110fe25607b2e19a9b5a /src/smt/process_assertions.cpp | |
| parent | 8badd4ee60ed4b221ce6db55ed641544f845149c (diff) | |
Fix support for global declarations (#7480)
Previously, we asserted global declarations as substitutions/formulas just before check-sat. This is not ideal since the current set of assertions can be preprocessed without having knowledge of definitions of defined functions. Moreover, this could lead to model unsoundness if it were the case that a defined symbol was solved during preprocessing.
Fixes #7479. In that example, y was solved for true and then we failed to overwrite y with its definition (> x 0), hence dropping the definition. Now, y is defined as (> x 0) before we preprocess.
Diffstat (limited to 'src/smt/process_assertions.cpp')
| -rw-r--r-- | src/smt/process_assertions.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 67e83bcd1..473b53015 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -93,6 +93,8 @@ void ProcessAssertions::spendResource(Resource r) bool ProcessAssertions::apply(Assertions& as) { + // must first refresh the assertions, in the case global declarations is true + as.refresh(); AssertionPipeline& assertions = as.getAssertionPipeline(); Assert(d_preprocessingPassContext != nullptr); // Dump the assertions |