diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-15 14:57:53 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-15 21:57:53 +0000 |
| commit | b7dcbee6f351c22ca3454d706d5773d01dd806fa (patch) | |
| tree | eef642fd1c9818ac32dd4dff7e13edfff6ff352c /test/regress | |
| parent | 640a07690826d4bbd87398949091b94b32e35c7a (diff) | |
preprocessing context: Add wrapper for model substitutions. (#6370)
Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.
Fixes #5473.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/v3l60006.cvc | 1 | ||||
| -rw-r--r-- | test/regress/regress0/issue5473.smt2 | 11 |
3 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a9b5174bb..12e0c568d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -638,6 +638,7 @@ set(regress_0_tests regress0/issue5187-div-justification.smt2 regress0/issue5370.smt2 regress0/issue5462.smt2 + regress0/issue5473.smt2 regress0/issue5540-2-dump-model.smt2 regress0/issue5540-model-decls.smt2 regress0/issue5550-num-children.smt2 diff --git a/test/regress/regress0/datatypes/v3l60006.cvc b/test/regress/regress0/datatypes/v3l60006.cvc index ea27672d5..8816caa9a 100644 --- a/test/regress/regress0/datatypes/v3l60006.cvc +++ b/test/regress/regress0/datatypes/v3l60006.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: -q % EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, diff --git a/test/regress/regress0/issue5473.smt2 b/test/regress/regress0/issue5473.smt2 new file mode 100644 index 000000000..bf24726f9 --- /dev/null +++ b/test/regress/regress0/issue5473.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: -q +; EXPECT: sat +; EXPECT: ((baz true)) +(set-logic QF_NIRA) +(set-option :produce-models true) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (! (or (= a (div 0 b))) :named baz)) +(assert (and (< b 5))) +(check-sat) +(get-assignment) |