Repository: testsmt/yinyang (language: python)

Issue:
Print warning when no solvers specified

Print warning when no solvers specified



Discussion / hints:

Fix patch:
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index e8c55ec..1516497 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -28,6 +28,7 @@ jobs:
     - name: Misc
       run: |
         python tests/integration_tests/misc/file_size_limit.py
+        python tests/integration_tests/misc/no_solvers.py
         python tests/integration_tests/misc/directory_mode.py
     - name: opfuzz
       run: |
diff --git a/src/args.py b/src/args.py
index 77ba901..afdd37e 100644
--- a/src/args.py
+++ b/src/args.py
@@ -109,7 +109,10 @@
 # pre-processing
 
 # Parse CLI
-if args.SOLVER_CLIS == "": args.SOLVER_CLIS = solvers
+if args.SOLVER_CLIS == "": 
+    if len(solvers) == 0:
+         exit("Error: no solver specified. Either change the commandline or edit config/config.py.")
+    args.SOLVER_CLIS = solvers
 else: args.SOLVER_CLIS = args.SOLVER_CLIS.split(";") + solvers
 
 if args.timeout <= 0: exit("Error: timeout should not be a negative number or zero.")


Test patch:
diff --git a/tests/integration_tests/detection/test_detection.py b/tests/integration_tests/detection/test_detection.py
index bd5df95..b5fd955 100644
--- a/tests/integration_tests/detection/test_detection.py
+++ b/tests/integration_tests/detection/test_detection.py
@@ -17,7 +17,7 @@ def is_sound(res1, res2):
 def call_fuzzer(first_config, second_config, fn, opts):
     cmd = python+' yinyang.py '+ '"'+ first_config+ ";" + second_config + '" ' + opts + ' ' + fn
     output = subprocess.getoutput(cmd)
-    print(output)
+    print(output,flush=True)
     crash_issues = None
     soundness_issues=None
     duplicate_issues=None
diff --git a/tests/integration_tests/misc/directory_mode.py b/tests/integration_tests/misc/directory_mode.py
index 3b752ad..f85a80c 100644
--- a/tests/integration_tests/misc/directory_mode.py
+++ b/tests/integration_tests/misc/directory_mode.py
@@ -46,7 +46,7 @@ def cleanup():
 first_config=z3+" model_validate=true"
 second_config=cvc4+" --check-models --produce-models --incremental -q"
 mock_benchmarks=str(os.path.dirname(os.path.realpath(__file__)))+"/mock_benchmarks"
-generated_seeds, used_seeds, ignored_issues, cmd = run_opfuzz(first_config, second_config, mock_benchmarks ,"",TIME_LIMIT)
+generated_seeds, used_seeds, ignored_issues, cmd = run_opfuzz(first_config, second_config, mock_benchmarks ,"-m 1",TIME_LIMIT)
 if not (generated_seeds == 300 and used_seeds == 3 and ignored_issues == 2):
     print("An error occurred.", flush=True)
     print("cmd", cmd)
diff --git a/tests/integration_tests/misc/no_solvers.py b/tests/integration_tests/misc/no_solvers.py
new file mode 100644
index 0000000..cd36794
--- /dev/null
+++ b/tests/integration_tests/misc/no_solvers.py
@@ -0,0 +1,17 @@
+import os
+import subprocess
+import sys
+
+python=sys.executable
+
+def call_fuzzer(fn):
+    cmd = python+' yinyang.py "" ' + fn 
+    output = subprocess.getoutput(cmd)
+    return output
+
+fn="examples/phi1.smt2"
+out = call_fuzzer(fn)
+if "Error: no solver specified" in out: 
+    exit(0)
+exit(1)
+