diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-03 05:27:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-03 10:27:20 +0000 |
| commit | 324434a74b35d0e58bdb551c9155e9fb32844d07 (patch) | |
| tree | ef0cc6130cf87c7cfa0f1461925dea6315f9a03f /test | |
| parent | 217a258f4b52d8776c344f9c3d0d9e79aec060a5 (diff) | |
Fix preregistration for floating point theory (#7558)
Preregistering terms must always add them to the equality engine of TheoryFp, otherwise there may be preregistered terms that do not occur in the equality engine of TheoryFp, thus leading to crashes during theory combination.
Fixes cvc5/cvc5-projects#329.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/proj-issue329-prereg-context.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ffc92c20e..7839dc7f2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -613,6 +613,7 @@ set(regress_0_tests regress0/fp/issue5734.smt2 regress0/fp/issue6164.smt2 regress0/fp/issue7002.smt2 + regress0/fp/proj-issue329-prereg-context.smt2 regress0/fp/rti_3_5_bug.smt2 regress0/fp/simple.smt2 regress0/fp/word-blast.smt2 diff --git a/test/regress/regress0/fp/proj-issue329-prereg-context.smt2 b/test/regress/regress0/fp/proj-issue329-prereg-context.smt2 new file mode 100644 index 000000000..f32a4ed33 --- /dev/null +++ b/test/regress/regress0/fp/proj-issue329-prereg-context.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --fp-exp +; EXPECT: sat +(set-logic ALL) +(declare-const x Float128) +(declare-const _x String) +(declare-fun x5 (Bool Float128) Bool) +(check-sat-assuming ((x5 (exists ((x (Array String Bool))) (and (select x _x) (or (select x _x) (x5 (exists ((x Bool)) true) (_ -oo 15 113))))) x))) |