summaryrefslogtreecommitdiff
path: root/test/regress/regress1
AgeCommit message (Collapse)Author
2021-06-02Merge branch 'master' into issue6661issue6661Andrew Reynolds
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-06-02Merge branch 'master' into issue6661Andres Noetzli
2021-06-02Fix unsat core proofs (#6655)Andrew Reynolds
Fixes cases of satisfiable unsat cores when proofs are enabled. Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.
2021-06-01Remove option to ignore negative membershipsAndres Noetzli
Fixes #6661. The option `--strings-inm` could be used to ignore negative membership constraints. However, this option made the string solver model-unsound or produced incorrect models if the user provided a benchmark that actually contained negative membership constraints. The solver did not check for negative membership constraints and did not warn the user about them. Because the option is not really being used, this commit removes it.
2021-05-28Disable `--jh-rlv-order` for slow regressions (#6633)Andres Noetzli
This commit adds --no-jh-rlv-order to two string regressions that take over 2 minutes to run in debug after #6613, which increases the overall regression runtime significantly.
2021-05-27Fix regular expression aggressive elim (#6627)Andrew Reynolds
Fixes #6620, fixes #6622. Fixes cvc5/cvc5-projects#254. The benchmarks from the 2 issues timeout, a regression is added for the projects issue.
2021-05-27Fix `str.replace_re` and `str.replace_re_all` (#6615)Andres Noetzli
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all` were not correctly enforcing that the operations replace the _first_ occurrence of some regular expression in a string. This commit fixes the issue by introducing a new operator `str.indexof_re(s, r, n)`, which, analoguously to `str.indexof`, returns the index of the first match of the regular expression `r` in `s`. The commit adds basic rewrites for evaluating the operator as well as its reduction. Additionally, it converts the reductions of `str.replace_re` and `str.replace_re_all` to use that new operator. This simplifies the reductions of the two operators and ensures that the semantics are consistent between the two.
2021-05-27Enable new justification heuristic by default (#6613)Andrew Reynolds
This enables the new implementation of justification heuristic by default. Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
2021-05-24Fix non-fixed length case in re-elim (#6612)Andrew Reynolds
Fixes followup issues from #6604.
2021-05-24Fix instance of no rewrite in extended rewriter (#6610)Andrew Reynolds
Fixes #6545. An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously. It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental. It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
This PR does two things: (1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model. (2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model. It also removes the unused command GetSynthSolutionCommand.
2021-05-19Pass empty vector when constructing re empty, fixes rewrite (#6576)Andrew Reynolds
Fixes #6567.
2021-05-19Adding regressions that failed on old unsat cores (#6574)Haniel Barbosa
We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.
2021-05-19Change the default unsat cores (#6571)Haniel Barbosa
This commit changes the default unsat cores to those based on solving-under-assumptions in the SAT solver and the (new) preprocessing proofs. The evaluation below on all the non-fp non-incremental SMT-LIB benchmarks, 120s timeout, shows the differences of the unsat cores based on the old proofs, the new ones based on SAT assumptions + preprocessing proofs, and the new ones based on SAT and preprocessing proofs. Note that the union of the last two is on par with the first. ``` status total solved sat unsat best timeout memout error uniq disagr time_cpu memory benchmark config AUFDTLIRA newUnsatCoresAssumps-safe/ ee 35 4 0 4 4 7 0 23 2 0 954.0 1267.5 newUnsatCoresProofs ok 35 31 0 31 25 4 0 0 0 0 894.1 1692.9 oldUnsatCores ok 35 32 0 32 30 3 0 0 1 0 799.2 1428.5 AUFLIA newUnsatCoresAssumps-safe/ ok 11 7 0 7 7 4 0 0 7 0 532.2 7604.4 newUnsatCoresProofs ok 11 4 0 4 1 6 0 0 0 0 829.0 12459.8 oldUnsatCores ok 11 4 0 4 3 6 0 0 0 0 818.2 7764.4 AUFLIRA newUnsatCoresAssumps-safe/ to 2 0 0 0 0 2 0 0 0 0 241.6 125.6 newUnsatCoresProofs ok 2 2 0 2 1 0 0 0 0 0 54.2 45.5 oldUnsatCores ok 2 2 0 2 2 0 0 0 0 0 49.4 79.7 AUFNIRA newUnsatCoresAssumps-safe/ ok 10 5 0 5 5 5 0 0 2 0 748.4 1630.0 newUnsatCoresProofs ok 10 4 0 4 0 6 0 0 0 0 850.7 2978.8 oldUnsatCores ok 10 8 0 8 5 2 0 0 1 0 502.7 2048.5 BV newUnsatCoresAssumps-safe/ ok 7 1 1 0 1 6 0 0 1 0 734.2 2065.0 newUnsatCoresProofs ok 7 6 3 3 4 1 0 0 0 0 246.7 1023.9 oldUnsatCores ok 7 6 3 3 3 1 0 0 0 0 248.6 992.0 LIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.9 47.7 newUnsatCoresProofs ok 1 1 0 1 1 0 0 0 0 0 0.3 6.5 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 0.3 5.3 LRA newUnsatCoresAssumps-safe/ ok 5 3 0 3 3 2 0 0 3 0 450.7 260.4 newUnsatCoresProofs ok 5 2 0 2 0 3 0 0 0 0 537.8 424.5 oldUnsatCores ok 5 2 0 2 2 3 0 0 0 0 533.8 298.5 NIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.8 22.0 newUnsatCoresProofs ok 1 1 0 1 0 0 0 0 0 0 46.3 48.0 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 43.3 40.3 QF_ABV newUnsatCoresAssumps-safe/ ok 105 70 59 11 70 35 0 0 63 0 8195.5 19363.3 newUnsatCoresProofs ok 105 34 24 10 17 71 0 0 5 0 11099.5 35756.7 oldUnsatCores ok 105 37 23 14 18 69 0 0 1 0 11198.0 26878.1 QF_ANIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1631.8 newUnsatCoresProofs ok 4 4 3 1 2 0 0 0 0 0 175.1 1513.6 oldUnsatCores ok 4 4 3 1 3 0 0 0 0 0 173.8 1495.1 QF_AUFLIA newUnsatCoresAssumps-safe/ ok 35 6 1 5 6 29 0 0 3 0 3718.4 524.1 newUnsatCoresProofs ok 35 24 4 20 1 11 0 0 0 0 2357.2 36556.0 oldUnsatCores ok 35 32 5 27 29 3 0 0 5 0 1857.6 10067.7 QF_AUFNIA newUnsatCoresAssumps-safe/ ok 3 1 0 1 1 2 0 0 0 0 324.7 543.6 newUnsatCoresProofs ok 3 2 2 0 1 1 0 0 1 0 223.1 509.0 oldUnsatCores ok 3 2 1 1 1 1 0 0 0 0 268.5 484.3 QF_AX newUnsatCoresAssumps-safe/ ok 12 1 0 1 1 11 0 0 0 0 1379.2 391.3 newUnsatCoresProofs ok 12 10 0 10 0 2 0 0 0 0 528.7 7433.9 oldUnsatCores ok 12 12 0 12 11 0 0 0 1 0 343.0 2855.2 QF_BV newUnsatCoresAssumps-safe/ ok 96 56 30 26 49 39 2 0 35 0 9248.2 98058.7 newUnsatCoresProofs ok 96 37 26 11 23 52 7 0 7 0 9781.9 135924.7 oldUnsatCores ok 96 50 29 21 24 43 3 0 7 0 9155.6 107216.0 QF_IDL newUnsatCoresAssumps-safe/ ok 109 51 39 12 43 58 0 0 33 0 10427.2 50846.5 newUnsatCoresProofs ok 109 33 32 1 2 76 0 0 0 0 11692.8 108963.1 oldUnsatCores ok 109 75 55 20 64 34 0 0 26 0 10088.1 53105.6 QF_LIA newUnsatCoresAssumps-safe/ ok 306 155 111 44 138 151 0 0 119 0 25346.4 50556.0 newUnsatCoresProofs ok 306 117 95 22 49 189 0 0 0 0 27092.6 122894.9 oldUnsatCores ok 306 187 110 77 152 119 0 0 34 0 24521.0 61261.1 QF_LRA newUnsatCoresAssumps-safe/ ok 72 39 20 19 38 33 0 0 31 0 7475.3 16892.2 newUnsatCoresProofs ok 72 31 16 15 2 41 0 0 0 0 7569.3 35658.7 oldUnsatCores ok 72 41 18 23 32 31 0 0 2 0 7243.2 20593.9 QF_NIA newUnsatCoresAssumps-safe/ ok 4389 2009 1862 147 2002 903 0 0 1931 0 163975.7 280779.3 newUnsatCoresProofs ok 4389 2326 2156 170 752 792 0 0 37 0 151051.9 387779.8 oldUnsatCores ok 4389 2394 2199 195 2174 730 0 0 81 0 146419.3 259669.8 QF_NRA newUnsatCoresAssumps-safe/ ok 135 65 57 8 57 70 0 0 45 0 10195.7 24701.4 newUnsatCoresProofs ok 135 71 49 22 35 64 0 0 5 0 10825.3 32982.8 oldUnsatCores ok 135 75 54 21 51 61 0 0 9 0 10865.3 27260.9 QF_RDL newUnsatCoresAssumps-safe/ ok 7 5 1 4 5 2 0 0 1 0 564.7 958.4 newUnsatCoresProofs ok 7 1 1 0 0 6 0 0 0 0 842.0 11029.6 oldUnsatCores ok 7 6 1 5 2 1 0 0 1 0 665.8 1982.6 QF_S newUnsatCoresAssumps-safe/ ok 5 1 1 0 0 4 0 0 0 0 603.3 191.4 newUnsatCoresProofs ok 5 5 5 0 2 0 0 0 0 0 161.9 285.8 oldUnsatCores ok 5 4 4 0 3 1 0 0 0 0 225.9 219.3 QF_SLIA newUnsatCoresAssumps-safe/ ok 258 74 67 7 70 184 0 0 64 0 27245.9 20290.4 newUnsatCoresProofs ok 258 179 163 16 47 79 0 0 6 0 18996.0 33722.6 oldUnsatCores ok 258 184 162 22 149 74 0 0 9 0 18395.8 23004.3 QF_UF newUnsatCoresAssumps-safe/ ok 29 25 0 25 6 4 0 0 2 0 2362.4 7504.3 newUnsatCoresProofs ok 29 0 0 0 0 28 1 0 0 0 3508.0 124190.7 oldUnsatCores ok 29 27 0 27 23 2 0 0 4 0 1866.3 13635.1 QF_UFBV newUnsatCoresAssumps-safe/ ok 2 2 0 2 1 0 0 0 1 0 189.5 1599.3 newUnsatCoresProofs to 2 0 0 0 0 2 0 0 0 0 241.8 1818.8 oldUnsatCores ok 2 1 0 1 1 1 0 0 0 0 193.7 1500.9 QF_UFIDL newUnsatCoresAssumps-safe/ ok 9 9 0 9 7 0 0 0 4 0 697.0 1133.0 newUnsatCoresProofs to 9 0 0 0 0 9 0 0 0 0 1088.0 14652.6 oldUnsatCores ok 9 5 0 5 2 4 0 0 0 0 848.5 2079.6 QF_UFLIA newUnsatCoresAssumps-safe/ ok 1 1 0 1 0 0 0 0 0 0 117.1 76.4 newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.9 208.5 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 110.6 127.7 QF_UFLRA newUnsatCoresAssumps-safe/ ok 7 4 1 3 0 0 3 0 0 0 266.6 55098.3 newUnsatCoresProofs mo 7 0 0 0 0 0 7 0 0 0 261.7 56000.0 oldUnsatCores ok 7 7 4 3 7 0 0 0 3 0 408.4 20933.4 QF_UFNIA newUnsatCoresAssumps-safe/ ok 48 21 19 2 21 4 0 0 20 0 592.3 880.6 newUnsatCoresProofs ok 48 27 22 5 18 4 0 0 1 0 641.4 1548.8 oldUnsatCores ok 48 26 21 5 26 7 0 0 1 0 887.5 1044.6 QF_UFNRA newUnsatCoresAssumps-safe/ ok 1 1 1 0 1 0 0 0 1 0 108.3 17.9 newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.8 19.0 oldUnsatCores to 1 0 0 0 0 1 0 0 0 0 120.8 14.7 UF newUnsatCoresAssumps-safe/ ok 21 5 0 5 5 16 0 0 5 0 2123.8 3168.7 newUnsatCoresProofs ok 21 13 0 13 6 8 0 0 0 0 1496.3 6617.8 oldUnsatCores ok 21 16 0 16 11 5 0 0 3 0 1443.3 3919.2 UFDT newUnsatCoresAssumps-safe/ ok 35 6 0 6 6 29 0 0 5 0 3777.0 4485.5 newUnsatCoresProofs ok 35 28 0 28 15 7 0 0 0 0 1416.9 4293.6 oldUnsatCores ok 35 30 0 30 26 5 0 0 1 0 1406.9 3188.5 UFDTLIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1640.5 newUnsatCoresProofs ok 4 4 0 4 1 0 0 0 0 0 139.3 942.3 oldUnsatCores ok 4 4 0 4 3 0 0 0 0 0 156.4 851.8 UFDTLIRA newUnsatCoresAssumps-safe/ ok 1 1 0 1 1 0 0 0 1 0 0.0 3.1 newUnsatCoresProofs ok 1 0 0 0 0 0 0 0 0 0 0.0 3.2 oldUnsatCores ok 1 0 0 0 0 0 0 0 0 0 0.0 2.7 UFDTNIRA newUnsatCoresAssumps-safe/ ok 10 3 0 3 3 6 0 0 3 0 754.8 1386.9 newUnsatCoresProofs ok 10 7 0 7 5 3 0 0 0 0 377.0 848.8 oldUnsatCores ok 10 7 0 7 7 3 0 0 0 0 376.5 563.4 UFLIA newUnsatCoresAssumps-safe/ ok 24 8 0 8 8 16 0 0 8 0 2231.6 3179.2 newUnsatCoresProofs ok 24 14 0 14 3 10 0 0 1 0 1915.5 5131.1 oldUnsatCores ok 24 15 0 15 14 9 0 0 2 0 1857.5 3479.7 UFNIA newUnsatCoresAssumps-safe/ ok 354 183 28 155 116 133 0 0 113 0 25941.4 839089.7 newUnsatCoresProofs ok 354 107 17 90 28 107 92 0 2 0 23496.9 1020258.1 oldUnsatCores ok 354 237 19 218 233 72 0 0 66 0 19906.9 914273.0 ```
2021-05-18Loop over terms to reconstruct instead of obligations. (#6504)Abdalrhman Mohamed
This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.
2021-05-17Improve integration of CAD with nl-Ext (#6542)Gereon Kremer
This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
2021-05-10Unify top-level substitutions and model substitutions (#6499)Andrew Reynolds
This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions. The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model. There is no reason to have these two things be separate.
2021-05-07Move slow regressions and update guidelines. (#6508)Aina Niemetz
This moves regression test that exceed the time limit of their respective level to the appropriate level. It further updates the guidelines in the README with information on how to properly categorize regression tests into levels (with time limits). Note: Test regress3/issue4717.smt2 was previously unsolved (unknown) and is now sat (Z3 agrees).
2021-04-30Use substitutions for implementing defined functions (#6437)Andrew Reynolds
This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions. In other words, the effect of: (define-fun f X t) is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when (= f (lambda X t)) was an equality solved by non-clausal simplification The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula. In this PR: define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline. Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit. The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions. The proof manager does not require a special case of using the define-function maps. Define-function maps are eliminated from SmtEngine. Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
2021-04-27Fix refutational soundness bug in quantifier prenexing (#6448)Andrew Reynolds
This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas. This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables. This was reported by Geoff Sutcliffe via a TPTP run.
2021-04-25More check models (#6439)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful. This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
2021-04-22Fix models for sygus-inference, bv2int, real2int (#6421)Andrew Reynolds
In each case, previously we were generating a define-fun, what we needed was to do a model substitution. This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.
2021-04-20Add instantiation pool feature to the API (#6358)Andrew Reynolds
This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.
2021-04-15Reenable regression for minimizing instantiations (#6367)Andrew Reynolds
2021-04-14Merge equivalent sub-obligations instead of discarding them. (#6353)Abdalrhman Mohamed
This PR modifies the behavior of the reconstruction algorithm when the term to reconstruct contains two or more equivalent sub-terms, but one is easier to reconstruct than the others. Since we do not know which one is easier to reconstruct by matching, we match against all sub-terms. If a solution is found for one sub-term, we use it to solve the others.
2021-04-14Warn about infeasible SyGuS conjectures (#6345)Andrew Reynolds
2021-04-09Add regressions for issue 6214 (#6305)Andrew Reynolds
Adds 3 of the 6 benchmarks from issue 6214, the 1st and 5th benchmarks timeout. Fixes #6214. These benchmarks were fixed by 3c98bb2.
2021-04-08Add benchmark for issue 5101 (#6301)Andrew Reynolds
Fixes #5101.
2021-04-08Add benchmark for issue 4400 (#6288)Andrew Reynolds
Fixes #4400.
2021-04-07Add benchmark for 6270 (#6283)Andrew Reynolds
2021-04-07Add benchmark for issue 4420 (#6286)Andrew Reynolds
Adds a benchmark that was previous sensitive to assertion order, fixes #4420.
2021-04-07Fixes for abducts (#6279)Andrew Reynolds
Fixes benchmarks 2 and 3 from #5848.
2021-04-06Add benchmark for issue 5942 (#6296)Andrew Reynolds
Fixes #5942. This benchmark was fixed by recent changes to ppRewrite.
2021-04-06Fix issue with lemma during equality engine iterator in sets (#6289)Andrew Reynolds
Fixes #4370.
2021-04-06Remove stdPrintAscii option (#6280)Andrew Reynolds
Fixes #4179.
2021-04-05Fix spurious antecedant for symbolic regular expressions (#6284)Andrew Reynolds
Fixes #6271. This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.
2021-04-05Add benchmark for issue 4412 (#6287)Andrew Reynolds
2021-04-05Enable UF when pre-skolem nested option is enabled (#6282)Andrew Reynolds
Fixes #4328.
2021-04-05Fix subtyping for sets care graph (#6278)Andrew Reynolds
We were getting types for set singleton/membership in a way that was unsafe for subtyping, which was leading to incorrectly computing care graphs for sets of reals. Fixes #5705.
2021-04-03Disable substring component contains in strip endpoints (#6266)Andrew Reynolds
Fixes the first benchmark from #6203.
2021-04-01Simplify caching of regular expression unfolding (#6262)Andrew Reynolds
This ensures that we always cache regular expressions in a user-dependent manner. Previously, we were erroneously caching in a SAT-dependent way for very rare cases when non-constant regular expressions were used. Since we never dependent on current assertions for the unfolding, there is no need to cache in the SAT context. This fixes the second benchmark from #6203. This PR also improves our traces for checking models in strings.
2021-04-01Add regression for issue 6191 (#6264)Andrew Reynolds
2021-03-30Implement simple tracking of instantiation lemmas (#6077)Andrew Reynolds
We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution. This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination. Fixes #5899.
2021-03-23Removing unused build options and deprecated proof compile flag (#6195)Haniel Barbosa
2021-03-23Replace old sygus term reconstruction algorithm with a new one. (#5779)Abdalrhman Mohamed
This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
2021-03-22Guard for non-unique skolems in term formula removal (#6179)Andrew Reynolds
In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map. Fixes #6132.
2021-03-21Simplify strings term registration (#6174)Andrew Reynolds
String terms may enter into the equality engine without appearing in assertions, due to eager context-dependent simplification internal to the equality engine (--strings-eager-eval). In rare cases, we did not catch when a new string constant appeared in the equality engine, meaning it would not be marked as relevant leading to bogus models in incremental mode. This makes it so that proxy variables are stored in a user-context dependent manner, which impacts when terms marked as having a proxy variable are registered. The PR also simplifies our policies for when string terms are registered slightly. Fixes #6072.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback