This file contains a summary of important user-visible changes.
-Changes since 1.8
-=================
+Changes since CVC4 1.8
+======================
New Features:
* New unsat-core production modes based on the new proof infrastructure
is the same as before, only with this word removed from the beginning.
* Building with Python 2 is now deprecated.
* Removed the option `--rewrite-divk` (now effectively enabled by default).
-
-
-Changes since 1.7
-=================
-
-New Features:
-* New C++ and Python API: CVC4 has a new, more streamlined API. We plan to
- make CVC4 1.8 the last version that ships with the legacy API.
-* Strings: Full support of the new SMT-LIB standard for the theory of strings,
- including:
- * Support for `str.replace_re`, `str.replace_re_all`, `str.is_digit`,
- `str.from_code`, `re.diff`, and `re.comp`
- * Support for new operator names (e.g. `str.in_re` instead of `str.in.re`),
- new escape sequences. The new syntax is enabled by default for smt2 files.
-* Support for syntax-guided synthesis (SyGuS) problems in the new API. C++
- examples of the SyGuS API can be found in `./examples/api/sygus_*.cpp`.
-* Support for higher-order constraints. This includes treating function sorts
- (constructible by `->`) as first-class sorts and handling partially applied
- function symbols. Support for higher-order constraints can be enabled by
- the option `--uf-ho`.
-* Support for set comprehension binders `comprehension`.
-* Eager bit-blasting: Support for SAT solver Kissat.
-
-Improvements:
-* API: Function definitions can now be requested to be global. If the `global`
- parameter is set to true, they persist after popping the user context.
-* Java/Python bindings: The bindings now allow users to catch exceptions
-* Arithmetic: Performance improvements
- * Linear solver: New lemmas inspired by unit-cube tests
- * Non-linear solver: Expanded set of axioms
-* Ackermannization: The Ackermannization preprocessing pass now supports
- uninterpreted sorts and as a result all QF_UFBV problems are supported in
- combination with eager bit blasting.
-
-Changes:
-* CVC language: Models printed in the CVC language now include an explicit end
- marker to facilitate the communication over pipes with CVC4.
-* API change: `SmtEngine::query()` has been renamed to
- `SmtEngine::checkEntailed()` and `Result::Validity` has been renamed to
- `Result::Entailment` along with corresponding changes to the enum values.
-* Java API change: The name of CVC4's package is now `edu.stanford.CVC4`
- instead of `edu.nyu.acsys.CVC4`.
-* The default output language is changed from CVC to SMT-LIB 2.6. The
- default output language is used when the problem language cannot be
- easily inferred (for example when CVC4 is used from the API).
-* Printing of BV constants: previously CVC4 would print BV constant
- values as indexed symbols by default and in binary notation with the
- option --bv-print-consts-in-binary. To be SMT-LIB compliant the
- default behavior is now to print BV constant values in binary
- notation and as indexed symbols with the new option
- --bv-print-consts-as-indexed-symbols. The option
- --bv-print-consts-in-binary has been removed.
-* Updated to SyGuS language version 2.0 by default. This is the last release
- that will support the SyGuS language version 1.0 (`--lang=sygus1`). A
- script is provided to convert version 1.0 files to version 2.0, see
- `./contrib/sygus-v1-to-v2.sh`.
-* Support for user-provided rewrite rule quantifiers have been removed.
-* Support for certain option aliases have been removed.
-* Support for parallel portfolio builds has been removed.
-
-Changes since 1.6
-=================
-
-New Features:
-* Proofs:
- * Support for bit-vector proofs with eager bitblasting (older versions only
- supported proofs with lazy bitblasting).
-* Strings:
- * Support for `str.replaceall` operator.
- * New option `--re-elim` to reduce regular expressions to extended string
- operators, resulting in better performance on regular expression benchmarks
- (enabled by default).
-* SyGuS:
- * Support for abduction (`--sygus-abduct`). Given a formula, this option uses
- CVC4's SyGuS solver to find a sufficient condition such that the
- conjunction of the condition and the formula is unsatisfiable.
- * Support for two new term enumerator strategies: variable agnostic
- (`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`).
- By default, CVC4 tries to choose the best term enumerator strategy
- automatically based on the input (`--sygus-active-gen=auto`).
- * Support for streaming solutions of increasingly smaller size when using the
- PBE solver (`--sygus-stream --sygus-pbe`). After the first solution is found
- and printed, the solver will continue to look for new solutions and print
- those, if any, that are smaller than previously printed solutions.
- * Support for unification-based techniques in non-separable specifications
- (`--sygus-unif`). For solving invariant problems a dedicate mode
- (`--sygus-unif-boolean-heuristic-dt`) is available that builds candidate
- solutions using heuristic decision tree learning.
-
-Improvements:
-* Strings:
- * Significantly better performance on string benchmarks over the core theory
- and those with extended string functions like substring, contains, and
- replace.
-
-Changes:
-* API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
- actual behavior.
-* Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
-* The CVC3 compatibility layer has been removed.
-* The build system now uses CMake instead of Autotools. Please refer to
- [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
- up-to-date instructions on how to build CVC4.
-
-Changes since 1.5
-=================
-
-New Features:
-* A new theory of floating points.
-* Novel approach for solving quantified bit-vectors (BV).
-* Eager bit-blasting: Support for SAT solver CaDiCaL.
-* A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
-* Support for transcendental functions (sin, cos, exp). In SMT2 input, this
- can be enabled by adding T to the logic (e.g., QF_NRAT).
-* Support for new operators in strings, including string inequality (str.<=)
- and string code (str.code).
-* Support for automated rewrite rule generation from sygus (*.sy) inputs using
- syntax-guided enumeration (option --sygus-rr).
-
-Improvements:
-* Incremental unsat core support.
-* Further development of rewrite rules for the theory of strings and regular
- expressions.
-* Many optimizations for syntax-guided synthesis, including improved symmetry
- breaking for enumerative search and specialized algorithms for
- programming-by-examples conjectures.
-
-Changes:
-* Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
- support for CryptoMinisat 5.
-* The LFSC proof checker now resides in its own repository on GitHub at
- https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore.
-
-Changes since 1.4
-=================
-
-* Improved heuristics for reasoning about non-linear arithmetic.
-* Native support for syntax-guided synthesis (sygus).
-* Support for many new heuristics for reasoning with quantifiers, including
- finite model finding.
-* Support for proofs for uninterpreted functions, arrays, bitvectors, and
- their combinations.
-* Performance improvements to existing theories.
-* A new theory of sets with cardinality and relations.
-* A new theory of strings.
-* Support for unsat cores.
-* Support for separation logic constraints.
-* Simplification mode "incremental" no longer supported.
-* Support for array constants in constraints.
-* Syntax for array models has changed in some language front-ends.
-* New input/output languages supported: "smt2.0" and "smtlib2.0" to
- force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5;
- "smt2.6" and "smtlib2.6" to force SMT-LIB v2.6;
- "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
- version 2.6. If an :smt-lib-version is set in the input, that overrides
- the command line.
-* Abstract values in SMT-LIB models are now ascribed types (with "as").
-* In SMT-LIB model output, real-sorted but integer-valued constants are
- now printed in accordance with the standard (e.g. "1.0").
-
-Changes since 1.3
-=================
-
-* CVC4 now supports libc++ in addition to libstdc++ (this especially
- helps on Mac OS Mavericks).
-* The LFSC proof checker has been incorporated into CVC4 sources.
-* Theory of finite sets, handling the MLSS fragment (singleton, union,
- intersection, set subtraction, membership and subset).
-* By default, CVC4 builds in "production" mode (optimized, with fewer
- internal checks on). The common alternative is a "debug" build, which
- is much slower. By default, CVC4 builds with no GPL'ed dependences.
- However, this is not the best-performing version; for that, you should
- configure with "--enable-gpl --best", which links against GPL'ed
- libraries that improve usability and performance. For details on
- licensing and dependences, see the README file.
-* Small API adjustments to Datatypes to even out the API and make it
- function better in Java.
-* Timed statistics are now properly updated even on process abort.
-* Better automatic handling of output language setting when using CVC4
- via API. Previously, the "automatic" language setting was sometimes
- (though not always) defaulting to the internal "AST" language; it
- should now (correctly) default to the same as the input language
- (if the input language is supported as an output language), or the
- "CVC4" native output language if no input language setting is applied.
-* The SmtEngine cannot be safely copied with the copy constructor.
- Previous versions inadvertently permitted clients to do this via the
- API. This has been corrected, copy and assignment of the SmtEngine
- is no longer permitted.
-
-Changes since 1.2
-=================
-
-New features:
-* SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
- previously missing
-* New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
-* Support in linear logics for /, div, and mod by constants (with the
- --rewrite-divk command line option).
-* Parsing support for TPTP's TFF and TFA formats.
-* A new theory of strings: word (dis-)equations, length constraints,
- regular expressions.
-* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
- resolved.
-* New :command-verbosity SMT option to silence success and error messages
- on a per-command basis, and API changes to Command infrastructure to
- support this.
-
-Behavioral changes:
-* It is no longer permitted to request model or proof generation if there's
- been an intervening push/pop.
-* User-defined symbols (define-funs) are no longer reported in the output
- of get-model commands.
-* Exit codes are now more standard for UNIX command-line tools. Exit code
- zero means no error---but the result could be sat, unsat, or unknown---and
- nonzero means error.
-
-API changes:
-* Expr::substitute() now capable of substituting operators (e.g.,
- function symbols under an APPLY_UF)
-* Numerous improvements to the Java language bindings
-
-Changes since 1.1
-=================
-
-* Real arithmetic now has three simplex solvers for exact precision linear
- arithmetic: the classical dual solver and two new solvers based on
- techniques for minimizing the sum of infeasibilities. GLPK can now be used
- as a heuristic backup to the exact precision solvers. GLPK must be enabled
- at configure time. See --help for more information on enabling these solvers.
-* added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
-* support for theory "alternates": new ability to prototype new decision
- procedures that are selectable at runtime
-* various bugfixes
-
-Changes since 1.0
-=================
-
-* bit-vector solver now has a specialized decision procedure for unsigned bit-
- vector inequalities
-* numerous important bug fixes, performance improvements, and usability
- improvements
-* support for multiline input in interactive mode
-* Win32-building support via mingw
-* SMT-LIB get-model output now is easier to machine-parse: contains (model...)
-* user patterns for quantifier instantiation are now supported in the
- SMT-LIBv1.2 parser
-* --finite-model-find was incomplete when using --incremental, now fixed
-* the E-matching procedure is slightly improved
-* Boolean terms are now supported in datatypes
-* tuple and record support have been added to the compatibility library
-* driver verbosity change: for printing all commands as they're executed, you
- now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
- allows tracing the solver's activities (with -v and -vv) without having too
- much output.
-* to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
- use -q. Previously, this would silence all output (including "sat" or
- "unsat") as well. Now, single -q silences messages and warnings, and
- double -qq silences all output (except on exception or signal).
+* Removed support for redundant logics ALL_SUPPORTED and QF_ALL_SUPPORTED,
+ use ALL and QF_ALL instead.
// quantified Boolean formulas only; we're done.
enableQuantifiers();
p += 3;
- } else if(!strcmp(p, "QF_ALL_SUPPORTED")) {
- // the "all theories included" logic, no quantifiers
- enableEverything();
- disableQuantifiers();
- arithNonLinear();
- p += 16;
} else if(!strcmp(p, "QF_ALL")) {
// the "all theories included" logic, no quantifiers
enableEverything();
disableQuantifiers();
arithNonLinear();
p += 6;
- } else if(!strcmp(p, "ALL_SUPPORTED")) {
- // the "all theories included" logic, with quantifiers
- enableEverything();
- enableQuantifiers();
- arithNonLinear();
- p += 13;
} else if(!strcmp(p, "ALL")) {
// the "all theories included" logic, with quantifiers
enableEverything();
Solver slv;
/* Setup some options for cvc5 */
- slv.setLogic("QF_ALL_SUPPORTED");
+ slv.setLogic("QF_ALL");
slv.setOption("produce-models", "true");
slv.setOption("incremental", "false");
def test_declare_separation_heap(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
integer = solver.getIntegerSort()
solver.declareSeparationHeap(integer, integer)
# cannot declare separation logic heap more than once
def test_get_separation_heap_term2(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
solver.setOption("incremental", "false")
solver.setOption("produce-models", "false")
checkSimpleSeparationConstraints(solver)
def test_get_separation_heap_term3(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
solver.setOption("incremental", "false")
solver.setOption("produce-models", "true")
t = solver.mkFalse()
def test_get_separation_heap_term4(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
solver.setOption("incremental", "false")
solver.setOption("produce-models", "true")
t = solver.mkTrue()
def test_get_separation_heap_term5(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
solver.setOption("incremental", "false")
solver.setOption("produce-models", "true")
checkSimpleSeparationConstraints(solver)
def test_get_separation_nil_term2(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
solver.setOption("incremental", "false")
solver.setOption("produce-models", "false")
checkSimpleSeparationConstraints(solver)
def test_get_separation_nil_term3(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
solver.setOption("incremental", "false")
solver.setOption("produce-models", "true")
t = solver.mkFalse()
def test_get_separation_nil_term4(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
solver.setOption("incremental", "false")
solver.setOption("produce-models", "true")
t = solver.mkTrue()
def test_get_separation_nil_term5(solver):
- solver.setLogic("ALL_SUPPORTED")
+ solver.setLogic("ALL")
solver.setOption("incremental", "false")
solver.setOption("produce-models", "true")
checkSimpleSeparationConstraints(solver)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun _substvar_301_ () Bool)
(declare-fun _substvar_300_ () Bool)
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((Pair 2)) ((par (T1 T2) ((mk-pair (first T1) (second T2))))))
(assert (= (mk-pair 0.0 0.0) (mk-pair 1.5 2.5)))
(check-sat)
; COMMAND-LINE:
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun t () (_ BitVec 16))
(assert (not (= t ((_ int2bv 16) (bv2nat t)))))
; COMMAND-LINE:
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun t () Int)
(assert (= (+ t 1) (bv2nat ((_ int2bv 16) t))))
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun t () (_ BitVec 16))
(assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65536))))
(set-option :global-declarations true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
; Tree type
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((PairIntInt 0)) ( ( (pair (firstPairIntInt Int)
(secondPairIntInt Int)) ) ))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-codatatypes ((Stream 0)) (((C (c Stream)) (D (d Stream)) (E (e Stream)))))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-codatatypes ((list 0)) (((cons (head Int) (tail list)))))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-sort a_ 0)
(declare-fun __nun_card_witness_0 () a_)
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun start!13 () Bool)
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-datatypes ((Data 1)) ((par (T) ((data (first T))))))
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-datatypes ((Pair 2)) ((par (T S) ((pair (first T) (second S))))))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((Unit 0)) (((u))))
(declare-fun x () Unit)
; EXPECT: sat
;(set-option :produce-models true)
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-datatypes ((RealTree 0)) (
(
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-sort term 0)
(declare-codatatypes ((llist_tree 0) (tree 0)) (
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-codatatypes ((Stream 0)) (((S (s Stream)))))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-datatypes ((DNat 0) (Nat 0)) (((dnat (data Nat)))
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
x : [ REAL, REAL ];
y : REAL;
; COMMAND-LINE: --decision=justification --no-unconstrained
; EXPECT: unsat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-fun _substvar_245_ () Bool)
(declare-fun _substvar_246_ () Bool)
(declare-fun _substvar_247_ () Bool)
; COMMAND-LINE: --fmf-fun
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(define-fun-rec f ((x Int)) Bool false)
(assert (not (f 0)))
(check-sat)
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort a 0)
(declare-datatypes ((tree 0)) (((Leaf (lab a)))))
; COMMAND-LINE: --finite-model-find
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort a 0)
(declare-datatypes ((prod 0)) (((Pair (gx a) (gy a)))))
(declare-fun p () prod)
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-fun cowlNothing ($$unsorted) Bool)
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-sort a 0)
(declare-fun __nun_card_witness_0 () a)
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-fun $$rtu (Real) $$unsorted)
; COMMAND-LINE: --fmf-fun --no-check-models
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort elem 0)
(declare-datatypes ((list 0)) (((Nil) (Cons (hd elem) (tl list)))))
(define-fun-rec f ((x list)) elem
-( set-logic QF_ALL_SUPPORTED)
+( set-logic QF_ALL)
( set-info :source | SMT-COMP'06 organizers |)
( set-info :smt-lib-version 2.6)
( set-info :category "check")
-( set-logic QF_ALL_SUPPORTED)
+( set-logic QF_ALL)
( set-info :source | SMT-COMP'06 organizers |)
( set-info :smt-lib-version 2.6)
( set-info :category "check")
; COMMAND-LINE: --incremental --fmf-fun --strings-exp
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((List_T_C 0) (T_CustomerType 0)) (
((List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C)))
((T_CustomerType$C_T_CustomerType (T_CustomerType$C_T_CustomerType$a_CompanyName Int) (T_CustomerType$C_T_CustomerType$a_ContactName Int) (ID Int)))
; COMMAND-LINE: --cegqi --dt-rewrite-error-sel
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
(assert (exists ((y Int)) (forall ((x List)) (not (= (head x) (+ y 7))))))
(check-sat)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(define-funs-rec ((is-even ((x Int)) Bool) (is-odd ((x Int)) Bool)) ((or (= x 0) (is-odd (- x 1))) (and (not (= x 0)) (is-even (- x 1)))))
; COMMAND-LINE: --purify-triggers
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-fun P (Int) Bool)
(assert (forall ((x Int)) (P (* 2 x))))
(assert (not (P 38)))
; COMMAND-LINE:
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun P (Real) Bool)
(assert (forall ((x Int)) (P x)))
; COMMAND-LINE: --partial-triggers
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun P (Int) Bool)
(assert (forall ((x Int) (y Int)) (=> (> y 6) (or (> x y) (P x)))))
; COMMAND-LINE: --cegqi
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((nat 0)) (( (Suc (pred nat)) (zero))))
(declare-fun y () nat)
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((Formula!953 0)) (((And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32))))))
(declare-fun error_value!964 () Bool)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(define-funs-rec (
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom : TYPE;
AtomTup : TYPE = [Atom];
AtomBinTup : TYPE = [Atom, Atom];
% EXPECT: unsat\r
OPTION "sets-ext";\r
-OPTION "logic" "ALL_SUPPORTED";\r
+OPTION "logic" "ALL";\r
Atom: TYPE;\r
\r
a : SET OF [Atom];\r
% EXPECT: unknown (INCOMPLETE)
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
ASSERT (CARD(TRANSPOSE(x)) > 0);
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom: TYPE;
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
% EXPECT: unsat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom:TYPE;
AtomPair: TYPE = [Atom, Atom];
x : SET OF AtomPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
OPTION "sets-ext";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntTup: TYPE = [INT];
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
e : IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT, INT, INT];
x : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT, INT, INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT, INT, INT, INT];
x : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT, INT, INT, INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT, INT];
IntTup: TYPE = [INT, INT, INT, INT,INT, INT];
x : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT, INT];
IntTup: TYPE = [INT, INT, INT, INT,INT, INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT, INT, INT, INT];
x : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
% crash on this
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
w : SET OF IntPair;
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
% crash on this
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
w : SET OF IntPair;
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT, INT, INT, INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
w : SET OF IntPair;
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntTup: TYPE = [INT, INT, INT];
x : SET OF IntTup;
y : SET OF IntTup;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntTup: TYPE = [INT, INT, INT];
x : SET OF IntTup;
y : SET OF IntTup;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
w : SET OF IntPair;
z : SET OF IntPair;
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-sort Loc 0)
(declare-const l Loc)
; EXPECT: (error "ERROR: the type of the separation logic heap has not been declared (e.g. via a declare-heap command), and we have a separation logic constraint (wand true true)
; EXPECT: ")
; EXIT: 1
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(assert (wand true true))
(check-sat)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-fun x () Int)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-sort U 0)
(declare-heap (U U))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-option :produce-models true)
(set-info :status sat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-heap (Int Int))
(assert (not (_ emp Int Int)))
(check-sat)
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-sort Loc 0)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-heap (Int Int))
(assert (wand (_ emp Int Int) (_ emp Int Int)))
(check-sat)
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
x : SET OF INT;
y : SET OF INT;
z : SET OF INT;
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun S () (Set Int))
(assert (>= (card S) 3))
% EXPECT: sat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom: TYPE;
a : SET OF [Atom];
b : SET OF [Atom];
% EXPECT: unsat\r
OPTION "sets-ext";\r
-OPTION "logic" "ALL_SUPPORTED";\r
+OPTION "logic" "ALL";\r
Atom: TYPE;\r
a : SET OF Atom;\r
b : SET OF Atom;\r
% EXPECT: sat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom : TYPE;
C32 : SET OF [Atom];
C2 : SET OF [Atom];
% EXPECT: unsat
% EXPECT: not_entailed
OPTION "incremental" true;
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
SetInt : TYPE = SET OF INT;
x : SET OF INT;
y : SET OF INT;
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((D 0)) (((A (a Int)))))
(declare-fun x1 () D)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(assert (member 5 (as emptyset (Set Int) )))
(check-sat)
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-fun A () (Set Int) )
(declare-fun B () (Set Int) )
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(assert (= (as emptyset (Set Int)) (singleton 5)))
(check-sat)
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun x () Int)
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
; Observed behavior
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
; Observed
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet ()
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun S () (Set Int))
(declare-fun T () (Set Int))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun x () Int)
(declare-fun y () Int)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(define-sort SetInt () (Set Int))
(declare-fun a () (Set Int))
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(define-sort SetInt () (Set Int))
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(define-sort SetInt () (Set Int))
; Something simple to test parsing
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun S () (Set Int))
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(define-sort SetInt () (Set Int))
(declare-fun a () (Set Int))
(declare-fun b () (Set Int))
; EXPECT: sat
; x not in A U B => x not in A
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(define-sort SetInt () (Set Int))
(declare-fun A () (Set Int))
(declare-fun B () (Set Int))
; EXPECT: sat
; x not in A U B => x not in A
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(define-sort SetInt () (Set Int))
(declare-fun A () (Set Int))
(declare-fun B () (Set Int))
; EXPECT: sat
; x not in A U B => x not in A
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(define-sort SetInt () (Set Int))
(declare-fun A () (Set Int))
(declare-fun B () (Set Int))
; EXPECT: sat
; x not in A U B => x not in A
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(define-sort SetInt () (Set Int))
(declare-fun A () (Set Int))
(declare-fun B () (Set Int))
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(define-sort SetInt () (Set Int))
(declare-fun A () (Set Int))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
(declare-fun s () String)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
(declare-fun s () String)
(set-info :smt-lib-version 2.6)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
(declare-const x Int)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status sat)
(declare-const x String)
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((IntRange 0))
(((IntRange (lower Int) (upper Int)))))
; COMMAND-LINE: -q
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; COMMAND-LINE: --finite-model-find --fmf-bound-int -q
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :incremental true)
(declare-fun P (Int) Bool)
; EXPECT: sat
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
; must make parts 1 through 6 with different deadlines
(set-info :smt-lib-version 2.6)
(set-info :status sat)
(set-option :produce-models true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
; done setting options
; Boogie universal background predicate
; COMMAND-LINE: --incremental
; EXPECT: sat
(set-option :produce-models true)
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-fun _substvar_1807_ () Bool)
(declare-fun local_id_x$1 () (_ BitVec 32))
(declare-fun local_id_x$2 () (_ BitVec 32))
; EXPECT: unknown
; EXPECT: unsat
; EXPECT: unknown
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((OptInt0 0)) (((Some (value0 Int)) (None))))
(declare-datatypes ((List0 0)) (((Cons (head0 Int) (tail0 List0)) (Nil))))
; EXIT: 1
; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays")
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-fun start!1 () Bool)
(assert start!1)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun t () Int)
(assert (> t 0))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun t () (_ BitVec 16))
(assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65535))))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun y () Int)
; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-datatypes ((Pair 2)) ((par (T S) ((pair (first T) (second S))))))
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((tuple2!879 0)) (((tuple2!879!880 (_1!881 Int) (_2!882 Int)))))
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((array!896 0)) (((array!896!897 (size!898 (_ BitVec 32)) (content!899 (Array (_ BitVec 32) (_ BitVec 32)))))))
(declare-datatypes ((tuple2!900 0)) (((tuple2!900!901 (_1!902 array!896) (_2!903 (_ BitVec 32))))))
; EXPECT: unsat
; Preamble --------------
(set-option :produce-models true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
;(declare-datatypes ((x2 0)) (((x1))))
(declare-datatypes ((x5 0)) (((x3) (x4))))
(declare-sort x6 0)
; COMMAND-LINE: --fmf-fun-rlv --no-check-models
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(define-fun $$isTrue$$ ((b Bool)) Bool b)
(define-fun $$isFalse$$ ((b Bool)) Bool (not b))
(define-fun $$toString$$ ((b Bool)) String (ite b "true" "false"))
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort U 0)
(declare-fun a () U)
(declare-fun b () U)
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort U 0)
(declare-fun a () U)
(declare-fun b () U)
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-sort U 0)
(declare-datatypes ((D 0)) (((cons (x Int) (y U)))))
; COMMAND-LINE: --finite-model-find --fmf-inst-engine
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-sort I_fb 0)
(declare-fun fb_arg_0_1 (I_fb) Int)
; EXPECT: sat
(set-option :produce-models true)
(set-option :interactive-mode true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort a 0)
(declare-datatypes ((w 0)) (((Wrap (unw a)))))
(declare-fun x () w)
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((St 0) (Ex 0) (List!2293 0))
(((Block!2236 (body!2237 List!2293)) (For!2238 (init!2239 St) (expr!2240 Ex) (step!2241 St) (body!2242 St)) (IfTE (expr!2244 Ex) (then!2245 St) (elze!2246 St)) (Skip!2250) (While (expr!2252 Ex) (body St)))
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((UNIT 0)) (((Unit))))
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
; COMMAND-LINE: --finite-model-find
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((UNIT 0)) (((Unit))))
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-sort a_ 0)
(declare-fun __nun_card_witness_0 () a_)
; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-sort a 0)
(declare-fun __nun_card_witness_0 () a)
; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil))))
(declare-fun app (Lst Lst) Lst)
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort b__ 0)
(declare-fun __nun_card_witness_0_ () b__)
(declare-sort a__ 0)
; COMMAND-LINE: --fmf-bound
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-const A (Set Int))
(declare-const B (Set Int))
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :smt-lib-version 2.6)
(set-info :category "unknown")
(set-info :status sat)
; COMMAND-LINE: --finite-model-find
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-sort g_ 0)
(declare-fun __nun_card_witness_0_ () g_)
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((Nat!2409 0)) (((succ!2410 (pred!2411 Nat!2409)) (zero!2412))
))
; COMMAND-LINE: --incremental --fmf-fun
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
(define-fun-rec sum ((l Lst)) Int (ite ((_ is nil) l) 0 (+ (head l) (sum (tail l)))))
; COMMAND-LINE: --sygus-inference
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-fun f (Int) Int)
(declare-fun a () Int)
; EXPECT: unsat
(set-option :incremental "false")
(set-info :status unsat)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-fun Y () String)
(set-info :notes "ufP_1 is uf type conv P")
(declare-fun ufP_1 (Int) Int)
; COMMAND-LINE: --full-saturate-quant
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-sort A$ 0)
(declare-sort A_set$ 0)
; COMMAND-LINE: --relational-triggers
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-sort U 0)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(define-funs-rec ((is-even ((x Int)) Int) (is-odd ((y Int)) Int)) ((ite (= x 0) 1 (ite (= (is-odd (- x 1)) 0) 1 0)) (ite (= y 0) 0 (ite (= (is-even (- y 1)) 0) 1 0))))
; EXPECT: in term : (R (as x (List Real)))")
; EXIT: 1
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil)))))
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((List 1)) ((par (T) ((cons (head T) (tail (List T))) (nil)))))
(declare-datatypes ((KV 0)) (((kv (key Int) (value Int)) (nilKV))))
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-sort A$ 0)
(declare-sort B$ 0)
; EXIT: 1
; this will fail if type rule for APPLY_UF requires arguments to be subtypes
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil)))))
; EXPECT: in term : (Q (as x (Array Int Real)))")
; EXIT: 1
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil)))))
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom : TYPE;
AtomTup : TYPE = [Atom];
AtomBinTup : TYPE = [Atom, Atom];
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom : TYPE;
AtomTup : TYPE = [Atom];
AtomBinTup : TYPE = [Atom, Atom];
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
DATATYPE unit = u END;
BvPair: TYPE = [BITVECTOR(1), unit, BITVECTOR(1)];
x : SET OF BvPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
DATATYPE unitb = ub(data : BITVECTOR(1)) END;
BvPair: TYPE = [BITVECTOR(1), unitb, BITVECTOR(1)];
x : SET OF BvPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
x : SET OF BvPair;
y : SET OF BvPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
x : SET OF BvPair;
y : SET OF BvPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
x : SET OF BvPair;
y : SET OF BvPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
BvPair: TYPE = [BITVECTOR(2), BITVECTOR(2)];
x : SET OF BvPair;
y : SET OF BvPair;
% EXPECT: sat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom:TYPE;
AtomPair: TYPE = [Atom, Atom];
x : SET OF AtomPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
OPTION "sets-ext";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
% EXPECT: sat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntPairPair: TYPE = [INT, INT, INT, INT];
x : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntPairPair: TYPE = [INT, INT, INT, INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT];
x : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT];
x : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [ INT, INT];
SetIntPair: TYPE = [ SET OF IntPair, SET OF IntPair ];
x : SET OF IntPair;
% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
IntPair: TYPE = [ INT, INT];
IntIntPair: TYPE = [ IntPair, IntPair];
x : SET OF IntIntPair;
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-sort Loc 0)
(declare-heap (Loc Loc))
; COMMAND-LINE: --quant-epr
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-sort U 0)
(declare-fun u () U)
; COMMAND-LINE: --finite-model-find --quant-epr
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort Loc 0)
(declare-const l Loc)
(declare-heap (Loc Loc))
; COMMAND-LINE: --finite-model-find --no-check-models
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort U 0)
(declare-heap (U Int))
(declare-fun u1 () U)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
; COMMAND-LINE: --full-saturate-quant
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
; COMMAND-LINE: --finite-model-find --quant-epr
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-sort Loc 0)
(declare-const l Loc)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-sort U 0)
(declare-heap (U U))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
; COMMAND-LINE:
; EXPECT: unsat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(declare-heap (Int Int))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-heap (Int Int))
(declare-fun x () Int)
(declare-fun y () Int)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
(declare-fun x () Int)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-heap (Int Int))
(declare-fun x () Int)
(assert (wand (_ emp Int Int) (pto x 3)))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
(declare-fun x () Int)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-heap (Int Int))
(declare-fun x () Int)
(assert (wand (pto x 1) (pto x 1)))
; COMMAND-LINE: --no-check-models
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(declare-heap (Int Int))
(declare-fun x () Int)
; COMMAND-LINE:
; EXPECT: unsat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(declare-fun x () Int)
(declare-heap (Int Int))
(assert (wand (pto x 1) (pto x 3)))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
; What was the bug?
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
(define-fun smt_set_emp () mySet (as emptyset mySet))
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
(define-fun smt_set_emp () mySet (as emptyset mySet))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(set-option :produce-models true)
(set-option :sets-ext true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(set-option :sets-ext true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(set-option :sets-ext true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(set-option :sets-ext true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(set-option :sets-ext true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(set-option :sets-ext true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(set-option :produce-models true)
(set-option :sets-ext true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(set-option :sets-ext true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(set-option :produce-models true)
(set-option :sets-ext true)
; COMMAND-LINE:
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun S () (Set Int))
(declare-fun x () Int)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
; conjecture set nonempty(~b & ~c)
; adding terms to d_pendingEverInserted was moved from addToPending()
; to getLemma().
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_ALL)
(set-info :status sat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
% COMMAND-LINE:
% EXPECT: sat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
a : SET OF [REAL, INT];
b : SET OF [INT, REAL];
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status unsat)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status sat)
(declare-fun s () String)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status sat)
(declare-fun s () String)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status unsat)
(declare-fun s () String)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
(declare-fun string () String)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(set-option :strings-exp true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status unsat)
(declare-const id String)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status unsat)
(declare-fun a () String)
(set-info :smt-lib-version 2.6)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status sat)
(declare-fun a () String)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status unsat)
(declare-fun a () String)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status sat)
(declare-const x String)
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-var m Int)
(declare-var s Int)
(declare-var inc Int)
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-active-gen=enum
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((IntRange 0))
(((IntRange (lower Int) (upper Int)))))
; EXPECT: unsat\r
; COMMAND-LINE: --lang=sygus2 --sygus-out=status\r
\r
-(set-logic ALL_SUPPORTED)\r
+(set-logic ALL)\r
(declare-datatype Ex ((Ex2 (ex Int))))\r
\r
(synth-fun ident ((x1 Ex)) Int\r
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatype Doc ((D (owner Int) (body Int))))
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
(set-option :print-success false)
(set-info :smt-lib-version 2.6)
;(set-option :produce-models true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
; done setting options
; Boogie universal background predicate
; COMMAND-LINE: --quant-ind --incremental
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite ((_ is nil) l1) l2 (cons (head l1) (app (tail l1) l2))))
(define-fun-rec rev ((l Lst)) Lst (ite ((_ is nil) l) nil (app (rev (tail l)) (cons (head l) nil))))
; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((Color 0)) (
((red) (white) (blue))
; COMMAND-LINE: -i -q\r
; EXPECT: unsat\r
-(set-logic ALL_SUPPORTED)\r
+(set-logic ALL)\r
(set-info :status unsat)\r
(declare-sort |T@[Int]Int| 0)\r
(declare-datatypes ((T@Vec_2846 0)) (((Vec_2846 (|v#Vec_2846| |T@[Int]Int|) (|l#Vec_2846| Int) ) ) ))\r
; EXPECT: unsat
; COMMAND-LINE: --finite-model-find
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((nat__ 0)) (((Suc__ (_select_Suc___0 nat__)) (zero__))))
(declare-sort a__ 0)
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-info :smt-lib-version 2.6)
(set-option :strings-exp true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(set-option :strings-exp true)
(set-option :strings-fmf true)
; COMMAND-LINE: --strings-exp --strings-fmf
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun url () String)
; COMMAND-LINE: --strings-exp
; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status sat)
(declare-fun url () String)
; Temporarily disable checking of unsat cores (see issue #3606)
; COMMAND-LINE: --no-check-unsat-cores
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-option :strings-exp true)
(set-info :status unsat)
(declare-fun a () String)
; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((Statement!1556 0) (Expression!1578 0) (List!1617 0)) (
((Assign!1557 (varID!1558 (_ BitVec 32)) (expr!1559 Expression!1578)) (Block!1560 (body!1561 List!1617)) (For!1562 (init!1563 Statement!1556) (expr!1564 Expression!1578) (step!1565 Statement!1556) (body!1566 Statement!1556)) (IfThenElse!1567 (expr!1568 Expression!1578) (then!1569 Statement!1556) (elze!1570 Statement!1556)) (Print!1571 (msg!1572 (_ BitVec 32)) (varID!1573 (_ BitVec 32))) (Skip!1574) (While!1575 (expr!1576 Expression!1578) (body!1577 Statement!1556)))
((And!1579 (lhs!1580 Expression!1578) (rhs!1581 Expression!1578)) (Division!1582 (lhs!1583 Expression!1578) (rhs!1584 Expression!1578)) (Equals!1585 (lhs!1586 Expression!1578) (rhs!1587 Expression!1578)) (GreaterThan!1588 (lhs!1589 Expression!1578) (rhs!1590 Expression!1578)) (IntLiteral!1591 (value!1592 (_ BitVec 32))) (LessThan!1593 (lhs!1594 Expression!1578) (rhs!1595 Expression!1578)) (Minus!1596 (lhs!1597 Expression!1578) (rhs!1598 Expression!1578)) (Modulo!1599 (lhs!1600 Expression!1578) (rhs!1601 Expression!1578)) (Neg!1602 (expr!1603 Expression!1578)) (Not!1604 (expr!1605 Expression!1578)) (Or!1606 (lhs!1607 Expression!1578) (rhs!1608 Expression!1578)) (Plus!1609 (lhs!1610 Expression!1578) (rhs!1611 Expression!1578)) (Times!1612 (lhs!1613 Expression!1578) (rhs!1614 Expression!1578)) (Var!1615 (varID!1616 (_ BitVec 32))))
(set-option :print-success false)
(set-info :smt-lib-version 2.6)
;(set-option :produce-models true)
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
; done setting options
; Boogie universal background predicate
TEST_F(TestApiBlackSolver, declareSeparationHeap)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
Sort integer = d_solver.getIntegerSort();
ASSERT_NO_THROW(d_solver.declareSeparationHeap(integer, integer));
// cannot declare separation logic heap more than once
TEST_F(TestApiBlackSolver, getSeparationHeapTerm2)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-models", "false");
checkSimpleSeparationConstraints(&d_solver);
TEST_F(TestApiBlackSolver, getSeparationHeapTerm3)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-models", "true");
Term t = d_solver.mkFalse();
TEST_F(TestApiBlackSolver, getSeparationHeapTerm4)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-models", "true");
Term t = d_solver.mkTrue();
TEST_F(TestApiBlackSolver, getSeparationHeapTerm5)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-models", "true");
checkSimpleSeparationConstraints(&d_solver);
TEST_F(TestApiBlackSolver, getSeparationNilTerm2)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-models", "false");
checkSimpleSeparationConstraints(&d_solver);
TEST_F(TestApiBlackSolver, getSeparationNilTerm3)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-models", "true");
Term t = d_solver.mkFalse();
TEST_F(TestApiBlackSolver, getSeparationNilTerm4)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-models", "true");
Term t = d_solver.mkTrue();
TEST_F(TestApiBlackSolver, getSeparationNilTerm5)
{
- d_solver.setLogic("ALL_SUPPORTED");
+ d_solver.setLogic("ALL");
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-models", "true");
checkSimpleSeparationConstraints(&d_solver);
ASSERT_FALSE(info.hasEverything());
ASSERT_FALSE(info.hasNothing());
- info = LogicInfo("QF_ALL_SUPPORTED");
+ info = LogicInfo("QF_ALL");
ASSERT_TRUE(info.isLocked());
ASSERT_FALSE(info.isPure(THEORY_BOOL));
ASSERT_TRUE(info.isSharingEnabled());
ASSERT_FALSE(info.hasEverything());
ASSERT_FALSE(info.hasNothing());
- info = LogicInfo("ALL_SUPPORTED");
+ info = LogicInfo("ALL");
ASSERT_TRUE(info.isLocked());
ASSERT_FALSE(info.isPure(THEORY_BOOL));
ASSERT_TRUE(info.isSharingEnabled());
projects / cvc5.git / commitdiff