From e9178fd85afff9bf5340b92e14efed6f805fb50f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 9 Nov 2020 11:35:39 +0100
Subject: [PATCH] Fix logic in tests

---
 tests/sat/repr2.smt2                     | 2 +-
 tests/sat/test-Top-Int_Pow1_invalid.smt2 | 2 +-
 tests/unsat/bug11.smt2                   | 2 +-
 tests/unsat/test-Top-Double1_valid.smt2  | 2 +-
 tests/unsat/test-Top-Double2_valid.smt2  | 2 +-
 tests/unsat/test-Top-G0_valid.smt2       | 2 +-
 tests/unsat/test-Top-G1_valid.smt2       | 2 +-
 tests/unsat/test-Top-G3_valid.smt2       | 2 +-
 tests/unsat/test-Top-G4_valid.smt2       | 2 +-
 tests/unsat/test-Top-Square1_valid.smt2  | 2 +-
 tests/unsat/test-Top-Square2_valid.smt2  | 2 +-
 11 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/tests/sat/repr2.smt2 b/tests/sat/repr2.smt2
index 07e2b88b0..a6f9426bc 100644
--- a/tests/sat/repr2.smt2
+++ b/tests/sat/repr2.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/sat/test-Top-Int_Pow1_invalid.smt2 b/tests/sat/test-Top-Int_Pow1_invalid.smt2
index f032f197c..4154e7f09 100644
--- a/tests/sat/test-Top-Int_Pow1_invalid.smt2
+++ b/tests/sat/test-Top-Int_Pow1_invalid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/bug11.smt2 b/tests/unsat/bug11.smt2
index 96c52c05c..cf4d4377b 100644
--- a/tests/unsat/bug11.smt2
+++ b/tests/unsat/bug11.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/test-Top-Double1_valid.smt2 b/tests/unsat/test-Top-Double1_valid.smt2
index dd8742789..01a38ee3a 100644
--- a/tests/unsat/test-Top-Double1_valid.smt2
+++ b/tests/unsat/test-Top-Double1_valid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/test-Top-Double2_valid.smt2 b/tests/unsat/test-Top-Double2_valid.smt2
index 988676ab7..7e2508e2e 100644
--- a/tests/unsat/test-Top-Double2_valid.smt2
+++ b/tests/unsat/test-Top-Double2_valid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/test-Top-G0_valid.smt2 b/tests/unsat/test-Top-G0_valid.smt2
index ca17ef951..ca119d470 100644
--- a/tests/unsat/test-Top-G0_valid.smt2
+++ b/tests/unsat/test-Top-G0_valid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/test-Top-G1_valid.smt2 b/tests/unsat/test-Top-G1_valid.smt2
index 2f11c9b10..1e7089c65 100644
--- a/tests/unsat/test-Top-G1_valid.smt2
+++ b/tests/unsat/test-Top-G1_valid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/test-Top-G3_valid.smt2 b/tests/unsat/test-Top-G3_valid.smt2
index fd2ad157b..28a2de971 100644
--- a/tests/unsat/test-Top-G3_valid.smt2
+++ b/tests/unsat/test-Top-G3_valid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/test-Top-G4_valid.smt2 b/tests/unsat/test-Top-G4_valid.smt2
index 07b0a8b20..26179cbc4 100644
--- a/tests/unsat/test-Top-G4_valid.smt2
+++ b/tests/unsat/test-Top-G4_valid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/test-Top-Square1_valid.smt2 b/tests/unsat/test-Top-Square1_valid.smt2
index 97a167f8c..4c9dd699a 100644
--- a/tests/unsat/test-Top-Square1_valid.smt2
+++ b/tests/unsat/test-Top-Square1_valid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/tests/unsat/test-Top-Square2_valid.smt2 b/tests/unsat/test-Top-Square2_valid.smt2
index c3ea3bb19..2420cca1a 100644
--- a/tests/unsat/test-Top-Square2_valid.smt2
+++ b/tests/unsat/test-Top-Square2_valid.smt2
@@ -1,5 +1,5 @@
 ;; produced by colibri.drv ;;
-(set-logic QF_NIRABVFP)
+(set-logic ALL)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
-- 
GitLab