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/regress0 | |
| 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/regress0')
| -rw-r--r-- | test/regress/regress0/datatypes/v3l60006.cvc | 1 | ||||
| -rw-r--r-- | test/regress/regress0/issue5473.smt2 | 11 |
2 files changed, 12 insertions, 0 deletions
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) |