smt tests verbosity set to 0

tnelson · Oct 17, 2024 · 740b65b · 740b65b
1 parent 050b654
commit 740b65b
Show file tree

Hide file tree

Showing 36 changed files with 36 additions and 2 deletions.
diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/ab_ai.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/ab_ai.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 /** This is a model of an address book as described on Page 23 of the software abstractions book.
  * The model has the following interesting constructs:

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/ab_dua.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/ab_dua.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 /** This is a model of an address book as described on Page 23 of the software abstractions book.
  * The model has the following interesting constructs:

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_0.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_0.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 ---------------- Signatures ----------------
 

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_1.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_1.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 ---------------- Signatures ----------------
 
 abstract sig Person {}

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_2.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_2.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 ---------------- Signatures ----------------
 
 abstract sig Person {}

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_3.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_3.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 ---------------- Signatures ----------------
 
 abstract sig Person {}

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_4.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/academia_4.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 ---------------- Signatures ----------------
 

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/birthday.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/birthday.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 /*
  * Birthday Book

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/cf_0.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/cf_0.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 /*
  * In his 1973 song, Paul Simon said "One Man's Ceiling Is Another Man's Floor".

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/family_1.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/family_1.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 abstract sig Person {
 	spouse: lone Person,

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/family_2.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/family_2.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 abstract sig Person {
 	spouse: lone Person,

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/fs_nda.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/fs_nda.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 /*
  * Model of a generic file system.

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/fs_sd.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/fs_sd.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 abstract sig Object {}
 

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/gp_nsf.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/gp_nsf.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 abstract sig Person {
 	father: lone Man,

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/gp_nsg.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/gp_nsg.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 abstract sig Person {
 	father: lone Man,

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/javatypes.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/javatypes.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 /*
  * A simple model of typing in Java.

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/library.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/library.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 sig Title{}
 sig Book {name: one Title}

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/loc_int.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/loc_int.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 
 abstract sig Thing {}

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/number_1.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/number_1.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 /*
  * Alloy model of paragraph numbering

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/railway.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/railway.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 /*
  * A simple model of a railway system. Trains sit on segments of tracks

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/set.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/set.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 sig Set {
 	elements: set Element

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/social_1.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/social_1.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 ---------------- Signatures ----------------
 

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/social_2.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/social_2.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 ---------------- Signatures ----------------
 

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/social_3.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/social_3.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 ---------------- Signatures ----------------
 

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/social_4.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/social_4.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 ---------------- Signatures ----------------
 

diff --git a/forge/tests/smt/smtlibtor/alloy_benchmarks/social_5.frg b/forge/tests/smt/smtlibtor/alloy_benchmarks/social_5.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 ---------------- Signatures ----------------
 

diff --git a/forge/tests/smt/smtlibtor/arity_testing.frg b/forge/tests/smt/smtlibtor/arity_testing.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 sig Mammal {}
 

diff --git a/forge/tests/smt/smtlibtor/bounds_instantation.frg b/forge/tests/smt/smtlibtor/bounds_instantation.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 abstract sig Position {}
 one sig Near extends Position {}

diff --git a/forge/tests/smt/smtlibtor/cardinality_testing.frg b/forge/tests/smt/smtlibtor/cardinality_testing.frg
@@ -2,6 +2,7 @@
 
 option backend smtlibtor
 option run_sterling off
+option verbose 0
 
 sig Person {
     age : one Int,

diff --git a/forge/tests/smt/smtlibtor/comprehension_testing.frg b/forge/tests/smt/smtlibtor/comprehension_testing.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 sig Person {
     parents : set Person,

diff --git a/forge/tests/smt/smtlibtor/finite_intset.frg b/forge/tests/smt/smtlibtor/finite_intset.frg
@@ -1,6 +1,6 @@
 #lang forge 
 option backend smtlibtor 
-option verbose 1 
+option verbose 0
 
 /**
   The semantics of "Int" under smtlibtor are not exactly the same 

diff --git a/forge/tests/smt/smtlibtor/int_cardinality_testing.frg b/forge/tests/smt/smtlibtor/int_cardinality_testing.frg
@@ -1,5 +1,6 @@
 #lang forge 
 option backend smtlibtor
+option verbose 0
 one sig Helper { x, y: one Int }
 test expect {
     emptyInt: {#Int = 0} is unsat

diff --git a/forge/tests/smt/smtlibtor/multiplicity_testing.frg b/forge/tests/smt/smtlibtor/multiplicity_testing.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 sig Person {
     age : one Int,

diff --git a/forge/tests/smt/smtlibtor/operator_testing.frg b/forge/tests/smt/smtlibtor/operator_testing.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor
+option verbose 0
 
 sig Name {}
 sig Date {}

diff --git a/forge/tests/smt/smtlibtor/optimize_testing.frg b/forge/tests/smt/smtlibtor/optimize_testing.frg
@@ -1,5 +1,5 @@
 #lang forge
-option verbose 3
+option verbose 0
 option backend smtlibtor
 
 ---------------------------------------------------------------------------------------------------

diff --git a/forge/tests/smt/smtlibtor/simple_s-exp_test.frg b/forge/tests/smt/smtlibtor/simple_s-exp_test.frg
@@ -1,6 +1,7 @@
 #lang forge
 
 option backend smtlibtor 
+option verbose 0
 
 sig Person {
     parent : set Person