[aimos] Do not log specification information for AIMOS.

src/aimos.ml

@@ -94,9 +94,6 @@ let build_command config_prover
       amplitude
   in
   let command = Whyconf.get_complete_command ~with_steps:false config_prover in
-  Logs.info (fun m ->
-    m "@[Specification to verify:\n%s@]"
-      (Stdio.In_channel.read_all (Unix.realpath aimos_config)));
   Re__Core.replace_string re_aimos_file ~by:aimos_config command
 
 let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"

tests/aimos.t

@@ -23,29 +23,3 @@ Test verify
   > end
   > EOF
   [caisar] Goal G: Valid
-
-  $ cat >> test <<EOF
-  > theory AIMOS_oracle
-  >   use TestNetwork.AsArray
-  >   use ieee_float.Float64
-  >   use caisar.DatasetClassification
-  >   use caisar.DatasetClassificationProps
-  > 
-  >   goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
-  > end
-  > EOF
-  $ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv --verbosity=info --log-category=specification test 2>&1 | awk '{if ($1 =="models_path:") {n=split ($2,a,"/");print "    "$1" "a[n-3]"/"a[n-2]"/"a[n-1]"/"a[n];} else print $0}'
-  [caisar][INFO] Specification to verify:
-  options:
-    plot: false
-    inputs_path: $TESTCASE_ROOT/test_data.csv
-    transformations:
-    - name: reluplex_rotation
-    custom_t_path: config/custom_transformations.py
-  models:
-  - defaults:
-      models_path: _build/default/tests/TestNetwork.nnet
-      out_mode: classif_min
-  
-  [caisar][INFO] Verification results for theory 'AIMOS_oracle'
-  [caisar] Goal G: Valid