Addressing issue #16 (warning when no solver is specified)

.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: |

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.")

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

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)

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)
+