Merge branch 'master' into privateGetprivateGet

20 files changed, 67 insertions, 37 deletions

diff --git a/test/regress/regress0/bug522.smt2 b/test/regress/regress0/bug522.smt2
index 3a9ea0eaa..ad6e526a8 100644
--- a/test/regress/regress0/bug522.smt2
+++ b/test/regress/regress0/bug522.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: sat
 ; EXPECT: sat
-(set-option :incremental "true")
+(set-option :incremental true)
 (set-logic QF_UF)
 
 (push 1)
diff --git a/test/regress/regress0/bv/bv-abstr-bug.smt2 b/test/regress/regress0/bv/bv-abstr-bug.smt2
deleted file mode 100644
index cc38075a9..000000000
--- a/test/regress/regress0/bv/bv-abstr-bug.smt2
+++ /dev/null
@@ -1,16 +0,0 @@
-; COMMAND-LINE: --bv-abstraction --bitblast=eager
-;
-; BV-abstraction should not be applied
-(set-logic QF_BV)
-(set-info :status sat)
-(declare-const a Bool)
-(declare-const b Bool)
-(declare-const c Bool)
-(declare-const d Bool)
-(assert
- (or
-  (and a b)
-  (and c d)
- )
-)
-(check-sat)
diff --git a/test/regress/regress0/bv/test-bv_intro_pow2.smt2 b/test/regress/regress0/bv/test-bv_intro_pow2.smt2
index e89dd4c50..65471a6b9 100644
--- a/test/regress/regress0/bv/test-bv_intro_pow2.smt2
+++ b/test/regress/regress0/bv/test-bv_intro_pow2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores --bv-solver=layered
+; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores
 (set-info :smt-lib-version 2.6)
 (set-logic QF_BV)
 (set-info :status unsat)
diff --git a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
index f38a3ce41..6ce1c41cd 100644
--- a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
+++ b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
@@ -4,7 +4,7 @@
 ; generated by Nunchaku
 (declare-sort i_ 0)
 (declare-fun __nun_card_witness_0_ () i_)
-(assert (fmf.card __nun_card_witness_0_ 2))
+(assert (_ fmf.card i_ 2))
 (declare-fun i2_ () i_)
 (declare-fun i1_ () i_)
 (declare-fun i3_ () i_)
diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2
index d1fd2301c..26c9b423f 100644
--- a/test/regress/regress0/fmf/fc-simple.smt2
+++ b/test/regress/regress0/fmf/fc-simple.smt2
@@ -6,7 +6,7 @@
 (declare-fun a () U)
 (declare-fun c () U)
 
-(assert (fmf.card c 2))
-(assert (not (fmf.card a 4)))
+(assert (_ fmf.card U 2))
+(assert (not (_ fmf.card U 4)))
 
 (check-sat)
diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2
index 2d4000e6e..b07c53077 100644
--- a/test/regress/regress0/fmf/fc-unsat-pent.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2
@@ -15,6 +15,6 @@
 (assert (not (= d e)))
 (assert (not (= e a)))
 
-(assert (fmf.card c 2))
+(assert (_ fmf.card U 2))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
index 0d438f718..404b3abea 100644
--- a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
@@ -7,8 +7,8 @@
 (declare-fun b () U)
 (declare-fun c () U)
 
-(assert (not (fmf.card a 2)))
+(assert (not (_ fmf.card U 2)))
 
 (assert (forall ((x U)) (or (= x a) (= x b))))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/fmf/issue4850-force-card.smt2 b/test/regress/regress0/fmf/issue4850-force-card.smt2
index 5aa7fc894..465584a83 100644
--- a/test/regress/regress0/fmf/issue4850-force-card.smt2
+++ b/test/regress/regress0/fmf/issue4850-force-card.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (declare-sort a 0)
 (declare-fun b () a)
-(assert (not (fmf.card b 1)))
+(assert (not (_ fmf.card a 1)))
 (check-sat)
diff --git a/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 b/test/regress/regress0/fmf/issue4872-qf_ufc.smt2
index c46bc1e28..c265dddcd 100644
--- a/test/regress/regress0/fmf/issue4872-qf_ufc.smt2
+++ b/test/regress/regress0/fmf/issue4872-qf_ufc.smt2
@@ -2,6 +2,6 @@
 (set-info :status sat)
 (declare-sort S0 0)
 (declare-const S0-0 S0)
-(assert (fmf.card S0-0 1))
-(assert (fmf.card S0-0 4))
+(assert (_ fmf.card S0 1))
+(assert (_ fmf.card S0 4))
 (check-sat)
diff --git a/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 b/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2
index a92f2f441..d032114ac 100644
--- a/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2
+++ b/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (declare-sort a 0)
 (declare-fun b () a)
-(assert (fmf.card b 2))
+(assert (_ fmf.card a 2))
 (check-sat)
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)))
diff --git a/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 b/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
new file mode 100644
index 000000000..7dc3188f2
--- /dev/null
+++ b/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
@@ -0,0 +1,10 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-const x6 Bool)
+(declare-const x Int)
+(declare-const b (-> Int Int Int))
+(declare-const c (-> Int Int))
+(assert (> (b 1 0) 0))
+(assert (= (c 0) (b 0 1)))
+(assert(= c (ite x6 (b 1) (b (+ 1 x)))))
+(check-sat)
diff --git a/test/regress/regress0/issue5550-num-children.smt2 b/test/regress/regress0/issue5550-num-children.smt2
index 75810699b..62d078b32 100644
--- a/test/regress/regress0/issue5550-num-children.smt2
+++ b/test/regress/regress0/issue5550-num-children.smt2
@@ -2,5 +2,5 @@
 (set-logic UFC)
 (declare-sort a 0)
 (declare-fun b () a)
-(assert (not (fmf.card b 1)))
-(check-sat)
\ No newline at end of file
+(assert (not (_ fmf.card a 1)))
+(check-sat)
diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2
index 2a464571c..41012f888 100644
--- a/test/regress/regress0/options/ast-and-sexpr.smt2
+++ b/test/regress/regress0/options/ast-and-sexpr.smt2
@@ -13,5 +13,6 @@
 (get-option :command-verbosity)
 ; There is no SMT option to get the verbosity of a specific command
 
-(set-info :source (0 1 True False x ""))
+(set-info :source (true false (- 15) 15 15.0 #b00001111 #x0f x |x 
+"| "" """"))
 (get-info :status)
diff --git a/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2 b/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2
index 56d8bc107..a4c3c29f6 100644
--- a/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2
+++ b/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --no-bv-eq-solver
 ; EXPECT: sat
 (set-logic QF_ALL)
 (declare-fun x () (_ BitVec 1))
 (assert (= (_ bv0 1) ((_ int2bv 1) (bv2nat x))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 b/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2
new file mode 100644
index 000000000..841e7392b
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-const x Real)
+(declare-const x4 Real)
+(declare-const x8 Bool)
+(assert (<= x4 x))
+(assert (not (xor (> x4 x) x8)))
+(check-sat)
diff --git a/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2
new file mode 100644
index 000000000..bc10e9cac
--- /dev/null
+++ b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2
@@ -0,0 +1,13 @@
+; EXPECT: unknown
+(set-logic ALL)
+(set-option :check-proofs true)
+(set-option :proof-check eager)
+(declare-const x Real)
+(assert
+    (and
+        (< 1.0 x)
+        (<= x (/ 0.0 0.0 x))
+        (<= (/ 0.0 0.0 x) x)
+    )
+)
+(check-sat)
diff --git a/test/regress/regress0/proofs/project-issue330-eqproof.smt2 b/test/regress/regress0/proofs/project-issue330-eqproof.smt2
new file mode 100644
index 000000000..1da778205
--- /dev/null
+++ b/test/regress/regress0/proofs/project-issue330-eqproof.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-const x String)
+(declare-const x1 Int)
+(set-option :check-proofs true)
+(declare-const _x String)
+(check-sat-assuming ((>= 0 (ite (= x (str.++ (str.from_code 0) (str.replace_all x (str.from_code 0) (str.++ (str.from_code 0) (str.from_code 0))) _x) (ite false x (str.++ _x _x _x)) x) x1 0))))
\ No newline at end of file
diff --git a/test/regress/regress0/push-pop/inc-define.smt2 b/test/regress/regress0/push-pop/inc-define.smt2
index 27261eff6..57f4d711c 100644
--- a/test/regress/regress0/push-pop/inc-define.smt2
+++ b/test/regress/regress0/push-pop/inc-define.smt2
@@ -4,6 +4,6 @@
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (check-sat)
-(define t (not (= x 0)))
+(define-const t Bool (not (= x 0)))
 (assert t)
 (check-sat)
diff --git a/test/regress/regress0/smtlib/issue4552.smt2 b/test/regress/regress0/smtlib/issue4552.smt2
index af8e0b948..8fcfabd5e 100644
--- a/test/regress/regress0/smtlib/issue4552.smt2
+++ b/test/regress/regress0/smtlib/issue4552.smt2
@@ -6,8 +6,8 @@
 (set-option :global-declarations true)
 
 (push)
-(define a true)
-(define (f (b Bool)) b)
+(define-const a Bool true)
+(define-fun f ((b Bool)) Bool b)
 (define-const a2 Bool true)
 
 (define-fun a3 () Bool true)