Adjust tests for windows

tests/typing/pass/smtlib/v2.6/attribute/dune

@@ -65,38 +65,6 @@
   (action (diff nest_pattern.expected nest_pattern.full)))
 
 
-; Test for nested_quant.smt2
-; Incremental test
-
-(rule
-   (target  nested_quant.incremental)
-   (deps    (:input nested_quant.smt2))
-   (package dolmen_bin)
-   (action (chdir %{workspace_root}
-            (with-outputs-to %{target}
-             (with-accepted-exit-codes (or 0 (not 0))
-              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
-(rule
-  (alias runtest)
-  (package dolmen_bin)
-  (action (diff nested_quant.expected nested_quant.incremental)))
-
-; Full mode test
-
-(rule
-   (target  nested_quant.full)
-   (deps    (:input nested_quant.smt2))
-   (package dolmen_bin)
-   (action (chdir %{workspace_root}
-            (with-outputs-to %{target}
-             (with-accepted-exit-codes (or 0 (not 0))
-              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
-(rule
-  (alias runtest)
-  (package dolmen_bin)
-  (action (diff nested_quant.expected nested_quant.full)))
-
-
 ; Test for simple_pattern.smt2
 ; Incremental test
 

tests/typing/pass/smtlib/v2.6/attribute/flags.dune

@@ -1 +0,0 @@
---debug

tests/typing/pass/smtlib/v2.6/attribute/let_seq.expected

@@ -1,20 +1,4 @@
-[logic][parsed][0-15] set-logic: ALL
-[logic][typed][0-15] other_1[0-15]:
-                       set-logic: ALL =
-                         { theories: core, arrays, bitv, floats, string,
-                                     int+real;
-                           features: { free_sorts : true;
-                                       free_functions : true;
-                                       datatypes : true;
-                                       quantifiers : true;
-                                       arithmetic : regular;
-                                       arrays : all; }; }]}
-
-[logic][parsed][16-79] antecedent: (let (x : 5) in (= x x){(:foo bar)})
-File "tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2", line 5, character 5-13:
-5 |      :foo bar
+File "tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2", line 7, character 5-13:
+7 |      :foo bar
          ^^^^^^^^
 Warning Unknown attribute (the attribtue was ignored): `:foo`
-[logic][typed][16-79] hyp_1[16-79]:
-                        hyp: let x/160 = 5/159 in x/160 = x/160
-

tests/typing/pass/smtlib/v2.6/attribute/let_seq.smt2

@@ -1,3 +1,5 @@
+; This tests that attributes are correctly taken into account
+; To do that, we rely on the unknown attribute warning
 (set-logic ALL)
 (assert
   (let ((x 5))

tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.expected

@@ -1,21 +1,4 @@
-[logic][parsed][0-15] set-logic: ALL
-[logic][typed][0-15] other_1[0-15]:
-                       set-logic: ALL =
-                         { theories: core, arrays, bitv, floats, string,
-                                     int+real;
-                           features: { free_sorts : true;
-                                       free_functions : true;
-                                       datatypes : true;
-                                       quantifiers : true;
-                                       arithmetic : regular;
-                                       arrays : all; }; }]}
-
-[logic][parsed][16-125] antecedent:
-                          (∀ (x : Int) .
-                            (∀ (y : Int) . (= x y)){(:pattern (sexpr x))})
-[logic][typed][16-125] hyp_1[16-125]:
-                         hyp:
-                           ∀ x/159 : int/4.
-                             { multi-trigger int/4 x/159; }
-                             (∀ y/160 : int/4. x/159 = y/160)
-
+File "tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2", line 9, character 5-13:
+9 |      :foo bar
+         ^^^^^^^^
+Warning Unknown attribute (the attribtue was ignored): `:foo`

tests/typing/pass/smtlib/v2.6/attribute/nest_pattern.smt2

@@ -1,10 +1,12 @@
+; This tests that attributes are correctly taken into account
+; To do that, we rely on the unknown attribute warning
 (set-logic ALL)
 (assert
   (forall ((x Int))
     (! (forall ((y Int))
           (= x y)
        )
-     :pattern (x)
+     :foo bar
     )
   )
 )

tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.expected

@@ -1,20 +1,4 @@
-[logic][parsed][0-15] set-logic: ALL
-[logic][typed][0-15] other_1[0-15]:
-                       set-logic: ALL =
-                         { theories: core, arrays, bitv, floats, string,
-                                     int+real;
-                           features: { free_sorts : true;
-                                       free_functions : true;
-                                       datatypes : true;
-                                       quantifiers : true;
-                                       arithmetic : regular;
-                                       arrays : all; }; }]}
-
-[logic][parsed][16-88] antecedent:
-                         (∀ (x : Int) . (= x x){(:pattern (sexpr x))})
-[logic][typed][16-88] hyp_1[16-88]:
-                        hyp:
-                          ∀ x/159 : int/4.
-                            { multi-trigger int/4 x/159; }
-                            (x/159 = x/159)
-
+File "tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2", line 7, character 5-13:
+7 |      :foo bar
+         ^^^^^^^^
+Warning Unknown attribute (the attribtue was ignored): `:foo`

tests/typing/pass/smtlib/v2.6/attribute/simple_pattern.smt2

@@ -1,8 +1,10 @@
+; This tests that attributes are correctly taken into account
+; To do that, we rely on the unknown attribute warning
 (set-logic ALL)
 (assert
   (forall ((x Int))
     (! (= x x)
-     :pattern (x)
+     :foo bar
     )
   )
 )