Skip to content

Commit 65209fd

Browse files
committed
Minor cleanup of some SMT2 files
- Replaced `ALL_SUPPORTED` (which is CVC4-specific) with `ALL` (which is part of the SMTLIB 2.5+ standard). - Added `incremental` option in an SMT2 file, which is required for using the `push` and `pop` commands in CVC4.
1 parent 1a360f6 commit 65209fd

File tree

3 files changed

+4
-3
lines changed

3 files changed

+4
-3
lines changed

regression/strings/test3/test-bv-to-int-onebyone.smt2

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
(set-option :produce-models true)
2-
(set-logic ALL_SUPPORTED)
2+
(set-option :incremental true)
3+
(set-logic ALL)
34

45
(declare-fun s () String)
56
(declare-fun s2 () String)

regression/strings/test3/test-bv-to-int.smt2

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
(set-option :produce-models true)
2-
(set-logic ALL_SUPPORTED)
2+
(set-logic ALL)
33

44
(declare-fun s () String)
55
(declare-fun s2 () String)

regression/strings/test3/test-int.smt2

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
(set-option :produce-models true)
2-
(set-logic ALL_SUPPORTED)
2+
(set-logic ALL)
33

44
(declare-fun s () String)
55
(declare-fun s2 () String)

0 commit comments

Comments
 (0)