diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-21 09:01:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-21 14:01:04 +0000 |
| commit | c0d4ac3d307b13c24471da5af2f916569a7f52b9 (patch) | |
| tree | bc458edc2a59fd3877e7952beb52d27997a15c8b /test | |
| parent | 09097cd3b9cd3233b938ace34f3513a16ac17f80 (diff) | |
Simplify strings term registration (#6174)
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.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6072-inc-no-const-reg.smt2 | 11 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 964e73fc0..a98ea84bb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2036,6 +2036,7 @@ set(regress_1_tests regress1/strings/issue5692-infer-proxy.smt2 regress1/strings/issue5940-skc-len-conc.smt2 regress1/strings/issue5940-2-skc-len-conc.smt2 + regress1/strings/issue6072-inc-no-const-reg.smt2 regress1/strings/issue6075-repl-len-one-rr.smt2 regress1/strings/issue6142-repl-inv-rew.smt2 regress1/strings/kaluza-fl.smt2 diff --git a/test/regress/regress1/strings/issue6072-inc-no-const-reg.smt2 b/test/regress/regress1/strings/issue6072-inc-no-const-reg.smt2 new file mode 100644 index 000000000..178c8f6ac --- /dev/null +++ b/test/regress/regress1/strings/issue6072-inc-no-const-reg.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: -i --strings-exp +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(declare-fun i4 () Int) +(declare-fun str5 () String) +(assert (= (str.++ str5 (str.from_int i4)) (str.++ "15" str5 "1"))) +(push) +(check-sat) +(pop) +(check-sat) |